proposition: Theorem mm_term_ind s : P // s ~~> se -> Q s.
proof: Proof. Proof using HQ0 HQ1. intros (H1 & H2). revert s H1; apply mm_special_ind; auto. intros i rho v j w' H1 H3 H4. apply HQ1 with (1 := H1); auto. split; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss)