simp
case left.refl
n : Nat
disjoint : 0 &&& n = 0
⊢ 0 + n = 0 ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n