export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>; export interface Comm_Base_Proof<B extends Op> { type: 'rewrite', left: Equation<Add<_0, B>, Add<B, _0>>; // 0 + b = b + 0 right: ChainRewrites<[ IdentityR<B>, // b = b + 0 Sym<Identity<B>>, // b + 0 = b + 0 Refl<Add<B, _0>>, // true ], this['left']>; }; export interface Comm_Inductive_Proof<A extends Op, B extends Op> { type: 'rewrite', left: Equation<Add<Succ<A>, B>, Add<B, Succ<A>>>; // succ(a) + b = b + succ(a) right: ChainRewrites<[ SumSucc<A, B>, // succ(a + b) = b + succ(a) Commutativity<A, B>, // succ(b + a) = b + succ(a) SumSuccR<B, A>, // succ(b + a) = succ(b + a) Refl<Succ<Add<B, A>>>, // true ], this['left']>; }; export namespace spec { export type commutativity = [ assert<VerifyEquation<Comm_Base_Proof<'B'>>>, assert<VerifyEquation<Comm_Inductive_Proof<'A', 'B'>>>, ] }