diff options
Diffstat (limited to 'theories/Init/Logic_Type.v')
| -rw-r--r-- | theories/Init/Logic_Type.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index bdec651da..1333f3545 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -28,7 +28,7 @@ Section identity_is_a_congruence. Variable f : A -> B. Variables x y z : A. - + Lemma identity_sym : identity x y -> identity y x. Proof. destruct 1; trivial. |