. exists x
case h.left
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single x)

case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)
case h.right
x y : Nat
p : ¬(IsSingle (Single x) ∧ IsSingle (Single y))
⊢ IsSingle (Single y)