From c6db95802c02d479d3607f8cfcb38f21c1e8c48c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Sep 2013 18:12:46 -0700 Subject: [PATCH] Make example 1 less symmetric Signed-off-by: Leonardo de Moura --- examples/ex1.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/ex1.lean b/examples/ex1.lean index 49983720c..39d11bffa 100644 --- a/examples/ex1.lean +++ b/examples/ex1.lean @@ -13,14 +13,14 @@ Variable d : N Variable e : N (* Add axioms stating facts about these variables *) -Axiom H1 : (a = b ∧ b = c) ∨ (a = d ∧ d = c) +Axiom H1 : (a = b ∧ b = c) ∨ (d = c ∧ a = d) Axiom H2 : b = e (* Proof that (h a b) = (h c e) *) Theorem T1 : (h a b) = (h c e) := DisjCases H1 (λ C1, CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2) - (λ C2, CongrH (Trans (Conjunct1 C2) (Conjunct2 C2)) H2) + (λ C2, CongrH (Trans (Conjunct2 C2) (Conjunct1 C2)) H2) (* We can use theorem T1 to prove other theorems *) Theorem T2 : (h a (h a b)) = (h a (h c e)) :=