diff options
Diffstat (limited to 'theories/Init/Logic.v')
-rw-r--r-- | theories/Init/Logic.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 968922737..b855154ac 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -654,7 +654,7 @@ Declare Right Step iff_trans. Section ex. Local Unset Implicit Arguments. Definition eq_ex_uncurried' {A : Type} (P : A -> Prop) {u1 v1 : A} {u2 : P u1} {v2 : P v1} - (pq : exists p : u1 = v1, eq_rect _ _ u2 _ p = v2) + (pq : exists p : u1 = v1, rew p in u2 = v2) : ex_intro P u1 u2 = ex_intro P v1 v2. Proof. destruct pq as [p q]. @@ -663,7 +663,7 @@ Section ex. Defined. Definition eq_ex' {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1) - (p : u1 = v1) (q : eq_rect _ _ u2 _ p = v2) + (p : u1 = v1) (q : rew p in u2 = v2) : ex_intro P u1 u2 = ex_intro P v1 v2 := eq_ex_uncurried' P (ex_intro _ p q). @@ -674,13 +674,13 @@ Section ex. := eq_ex' u1 v1 u2 v2 p (P_hprop _ _ _). Lemma eq_rect_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : ex (Q x)) {y} (H : x = y) - : eq_rect x (fun a => ex (Q a)) u y H + : rew [fun a => ex (Q a)] H in u = match u with | ex_intro _ u1 u2 => ex_intro (Q y) - (eq_rect x P u1 y H) - match H in (_ = y) return Q y (eq_rect x P u1 y H) with + (rew H in u1) + match H in (_ = y) return Q y (rew H in u1) with | eq_refl => u2 end end. |