{ apply And.left h }
case mpr.left
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x

case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x
case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x