proposition: Lemma igotos_capped {i n X Y} : In (i, (n, X, Y)) igotos -> n < 4.
proof: Proof. Proof using capped_P. move /in_combine_r. rewrite /gotos ?in_app_iff ?in_map_iff. case; first by (move=> [[? [? ?]]] [[]] *; subst; apply: iP_capped; eassumption). do 4 (case; first by (move=> [[? [? ?]]] [[]] *; subst; lia)). case; last done. case=> *. by lia. Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun