variables p q r: Prop -- 1ª demostración example (h : p ∨ q) : q ∨ p := or.elim h (assume hp : p, show q ∨ p, from or.intro_right q hp) (assume hq : q, show q ∨ p, from or.intro_left p hq) -- 2ª demostración example (h : p ∨ q) : q ∨ p := or.elim h (λ hp, or.inr hp) (λ hq, or.inl hq) -- 3ª demostración example (h : p ∨ q) : q ∨ p := h.elim (assume hp : p, or.inr hp) (assume hq : q, or.inl hq)