proposition: Lemma confluence : confluent M' <-> confluent M.
proof: Proof. constructor; apply: confluent_incl; rewrite /M /M' => ?; rewrite /= ?in_app_iff /=; by firstorder done. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun