proposition: Lemma forward_add: m + n = p -> sigma • fst (addEQ x y z) ≡ sigma • snd (addEQ x y z).
proof: Proof. Proof using Ex Ey Ez. intros <-; cbn. unfold funcomp; change shift with (add 1); rewrite !ren_plus_combine; unfold var_zero; cbn. erewrite Ex, Ey, Ez; now simplify. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)