Slides of a (very) informal lecture of mine on the Curry-Howard correspondence
1 lemma ex : or p q → or q p := by 2 intro h 3 match h with 4 | inl h1 => 5 exact inr h1 6 | inr h2 => 7 exact inl h2