9 lines
213 B
Lean4
9 lines
213 B
Lean4
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
|