proposition: Lemma forward_mul: m * n = p -> sigma (G x y z) = T n m -> sigma • fst (mulEQ x y z) ≡ sigma • snd (mulEQ x y z).
proof: Proof. Proof using Ex Ey Ez. intros H1 H2. unfold mulEQ; cbn. unfold funcomp. rewrite H2. change shift with (add 1); rewrite !ren_plus_combine; cbn [plus]. rewrite Ex, Ey, Ez. subst p. eapply G_forward. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)