proposition: Lemma confluent_incl {M1 M2} : incl M1 M2 -> incl M2 M1 -> confluent M1 -> confluent M2.
proof: Proof. move=> /reachable_incl H12 /reachable_incl H21 HM1 ? ? ? /H21 /HM1 {}HM1 /H21 /HM1 [? [? ?]]. eexists. constructor; apply: H12; by eassumption. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun