variables (α : Type) (p q : α → Prop) -- 1ª demostración example : (∀ x : α, p x ∧ q x) → ∀ y : α, p y := assume h : ∀ x : α, p x ∧ q x, assume y : α, show p y, from (h y).left -- 2ª demostración example : (∀ x : α, p x ∧ q x) → ∀ x : α, p x := assume h : ∀ x : α, p x ∧ q x, assume z : α, show p z, from and.elim_left (h z)