lean.lean 213 B

123456789
  1. import logic
  2. section
  3. variables (A : Type) (p q : A → Prop)
  4. example : (∀x : A, p x ∧ q x) → ∀y : A, p y :=
  5. assume H : ∀x : A, p x ∧ q x,
  6. take y : A,
  7. show p y, from and.elim_left (H y)
  8. end