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)) :=