Equational reasoning in Haskell (w/ or w/o singleton types)

Proof.hs

plusCommutative :: SNat n -> SNat m -> Eql (n :+: m) (m :+: n)
plusCommutative SZ SZ     = Eql
plusCommutative SZ (SS m) =
  case plusZR (SS m) of
    Eql -> Eql
plusCommutative (SS n) m =
  case plusCommutative n m of
    Eql -> case sAndPlusOne (m %+ n) of
             Eql -> case plusAssociative m n sOne of
                      Eql -> case sAndPlusOne n of
                               Eql -> Eql

plusComm :: forall m n. SNat m -> SNat n -> m :+ n :=: n :+ m
plusComm m = induction' (Proxy :: Proxy (Comm m)) base cases
  where
    base :: BaseType (Comm m) Zero
    base =
      start (m %:+ sZero)
        =~= m
        === sZero %:+ m `because` symmetry (plusZeroL m)
    cases :: SuccCaseW (Comm m)
    cases hypo (SSucc n) =
      start (m %:+ sSucc n)
        =~= sSucc (m %:+ n)
        === sSucc (n %:+ m) `because` cong' sSucc (hypo n)
        =~= n %:+ sSucc m
        === sSucc n %:+ m   `because` nPlusSuccm n m