module exampleproofproplogic9 where


data _∨_  (A B : Set) : Set where
  or1 : A -> A ∨ B
  or2 : B -> A ∨ B

postulate A : Set
postulate B : Set

lemma3 : A ∨ B -> B ∨ A
lemma3 (or1 a) = or2 a
lemma3 (or2 b) = or1 b