diff options
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 76807b06bb..75043c4229 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -632,11 +632,8 @@ Proof. destruct (AC_depfun A0 B0 R0 H0) as (f, Hf). apply H. intros A P H'. - exists (f (existT (fun _ => sigT _) A - (existT (fun P => exists x, P x) P H'))). - pose (Hf' := - Hf (existT (fun _ => sigT _) A - (existT (fun P => exists x, P x) P H'))). + exists (f (existT _ A (existT _ P H'))). + pose (Hf' := Hf (existT _ A (existT _ P H'))). assumption. Qed. @@ -664,11 +661,8 @@ Proof. destruct (DepFunReify A0 B0 R0 H0) as (f, Hf). apply H. intros A P H'. - exists (f (existT (fun _ => sigT _) A - (existT (fun P => exists! x, P x) P H'))). - pose (Hf' := - Hf (existT (fun _ => sigT _) A - (existT (fun P => exists! x, P x) P H'))). + exists (f (existT _ A (existT _ P H'))). + pose (Hf' := Hf (existT _ A (existT _ P H'))). assumption. Qed. |