proposition: Lemma KM_MMA_iff {tm} : (forall sigma, Lambda.subst sigma tm = tm) -> KrivineM_HALT tm <-> @MMA_HALTING 5 (KM_MMA.PROG 1, KM_MMA.input tm).
proof: Proof. move=> /Krivine_facts.eclosed_closed ?. split. - by apply: KM_MMA.simulation. - by apply: (KM_MMA.inverse_simulation List.nil List.nil). Qed.
imports: Undecidability(TM.UTM TM.TM LambdaCalculus.Krivine MinskyMachines.MMA Shared.Libs.PSL.FiniteTypes.FinTypesDef) Coq(Vector ssreflect ssrbool ssrfun)