diff options
| -rw-r--r-- | theories/Init/Logic.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9d60cf54c3..67cbd5d0f7 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -406,6 +406,19 @@ End EqNotations. Import EqNotations. +Section equality_dep. + Variable A : Type. + Variable B : A -> Type. + Variable f : forall x, B x. + Variables x y : A. + + Theorem f_equal_dep : forall (H: x = y), rew H in f x = f y. + Proof. + destruct H; reflexivity. + Defined. + +End equality_dep. + Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a. Proof. intros. |