proposition: Lemma M_iff m p M: (m * n = p /\ M = T m) <-> Mrel m p M.
proof: Proof. split. - intros [<- ->]. apply M_forward. - intros H. specialize (M_backward_exists H) as [l ->]. eapply M_backward_equations in H; intuition. Qed.
imports: List Lia Undecidability.HOU(std.std axioms)