blob: 30e7efa63f46a1aea1ba9d583b3608509fa3a0bb [file] [edit]
case hp
p q : Prop
a : p ∧ q
⊢ p
case hp
p q : Prop
x✝ : p ∧ q
a : p
b : q
⊢ p
case hp
p q : Prop
x✝ : p ∧ q
a : p
b : q
⊢ p