proposition: Lemma simulation {x y} : reachable M' x y <-> reachable M x y.
proof: Proof. Proof using derivable. clear non_nil. constructor; last by (apply: reachable_incl; apply /incl_appr). elim. - move=> ? ?. case=> >. rewrite /M' in_app_iff. case. * case; last done. move=> [] *. subst. by apply: reachable_stack_app. * move=> ?. apply: rt_step. by apply: transition. - move=> *. by apply: rt_refl. - move=> *. apply: rt_trans; by eassumption. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun