proposition: Lemma M_backward_equations m p l : Mrel m p (T l) -> m = l /\ m * n = p.
proof: Proof. unfold Mrel. rewrite <-M_forward. intros H % app_injective; intuition; congruence. Qed.
imports: List Lia Undecidability.HOU(std.std axioms)