variables p q : Prop -- 1ª demostración example (hp : p) : p ∨ q := or.intro_left q hp -- 2ª demostración example (hp : p) : p ∨ q := or.inl hp