Set: pp::colors
  Set: pp::unicode
  Imported 'macros'
  Using: Nat
  Assumed: Induction
Failed to solve
 ⊢ ∀ m : ℕ, 0 + m == m + 0 ≺ ?M::3 0
    (line: 10: pos: 3) Type of argument 2 must be convertible to the expected type in the application of
        Induction
    with arguments:
        ?M::3
        λ m : ℕ, Nat::add::zerol m ⋈ symm (Nat::add::zeror m)
        λ (n : ℕ) (iH : ?M::3 n) (m : ℕ),
          Nat::add::succl n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succr m n)