diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic_Type.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index faeecdf9d..f5cee92c7 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -32,17 +32,17 @@ Section identity_is_a_congruence. Lemma sym_id : identity x y -> identity y x. Proof. destruct 1; trivial. - Qed. + Defined. Lemma trans_id : identity x y -> identity y z -> identity x z. Proof. destruct 2; trivial. - Qed. + Defined. Lemma congr_id : identity x y -> identity (f x) (f y). Proof. destruct 1; trivial. - Qed. + Defined. Lemma sym_not_id : notT (identity x y) -> notT (identity y x). Proof. |