diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-24 16:38:52 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-28 09:38:36 -0400 |
| commit | 37ff7235fe4d489a35458bb12abdf497480cf5c5 (patch) | |
| tree | 71458ce64ff5b29e71523e5d1a4922d0db929e89 /theories/Init | |
| parent | 9922c243e6d6a01d7308a6b1ce2aefd44d1b100e (diff) | |
Make new proofs of equality Qed
As requested in
https://github.com/coq/coq/pull/384#issuecomment-303809461
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 845b8ee9f..4c0c18772 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -507,7 +507,7 @@ Defined. Lemma eq_refl_map_distr : forall A B x (f:A->B), f_equal f (eq_refl x) = eq_refl (f x). Proof. reflexivity. -Defined. +Qed. Lemma eq_trans_map_distr : forall A B x y z (f:A->B) (e:x=y) (e':y=z), f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e'). Proof. @@ -531,13 +531,13 @@ Lemma eq_trans_rew_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k: rew (eq_trans e e') in k = rew e' in rew e in k. Proof. destruct e, e'; reflexivity. -Defined. +Qed. Lemma rew_const : forall A P (x y:A) (e:x=y) (k:P), rew [fun _ => P] e in k = k. Proof. destruct e; reflexivity. -Defined. +Qed. (* Aliases *) |