{ exact Or.inr λ hq => hnand ⟨h, hq⟩}
case pos
p q r : Prop
hnand : ¬(p ∧ q)
h : p
⊢ ¬p ∨ ¬q

case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q
case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q