variables p q : Prop -- 1ª demostración example (h : p ∧ q) : p := and.elim_left h -- 2ª demostración example (h : p ∧ q) : p := and.left h -- 3ª demostración example (h : p ∧ q) : p := h.left