//Macros UZero[]. USucc[prev]. Sub[a, b]. Neg[a]. Nat[]. Untyped[]. Zero[]. Succ[prev]. Add[a, b]. //Macros UZero[]: Zero[] | Untyped[] USucc[prev]: Succ[prev: prev<USucc] | Untyped[] Neg[a: Sub[a: Neg[a], b: Neg[a]]]: Add[ a: a<Neg>a<Sub>a<Neg b: a<Neg>b<Sub>a<Neg ] --- Add[a: Nat[], b: Nat[]] | Untyped[]: Nat[] Neg[a: Sub[a: Neg[a: Zero[]], b: Neg[a]]]: a<Neg>b<Sub>a<Neg Add[a: Succ[prev], b]: Add[a: a<Add>prev<Succ, b: Succ[prev: b<Add]] UZero[]: Zero[] | Nat[] USucc[prev: Nat[]]: Nat[] Add[ a: Succ[prev: Succ[prev: Succ[prev: Zero[] | Untyped[]] | Untyped[]] | Untyped[]] | Untyped[] b: Succ[prev: Succ[prev: Zero[] | Untyped[]] | Untyped[]] | Untyped[] ] | Untyped[]?