proposition: Lemma backward_mult: sigma • fst (mulEQ x y z) ≡ sigma • snd (mulEQ x y z) -> m * n = p /\ sigma (G x y z) = T n m.
proof: Proof. Proof using N Ex Ey Ez. unfold mulEQ; cbn. unfold funcomp. change shift with (add 1); rewrite !ren_plus_combine; cbn [plus]. rewrite Ex, Ey, Ez. intros H. apply G_iff in H; (eauto 2). Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)