diff options
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Init/Logic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 545c0acb7..ec1d850e0 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -114,7 +114,7 @@ Section Logic_lemmas. Variable x,y,z : A. Theorem sym_eq : (eq ? x y) -> (eq ? y x). - Proof. + Proof. Induction 1; Trivial. Qed. |