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

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