import logic
section
variables (A : Type) (p q : A → Prop)
example : (∀x : A, p x ∧ q x) → ∀y : A, p y :=
assume H : ∀x : A, p x ∧ q x,
take y : A,
show p y, from and.elim_left (H y)
end