proposition: Lemma mm2_state_eta (x : mm2_state) : x = (index x, (value1 x, value2 x)).
proof: Proof. by move: x => [? [? ?]]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun