proposition: Lemma encode_decode_Stack {s: list bool} : encode_Stack (decode_Stack s) = s.
proof: Proof. rewrite /encode_Stack /decode_Stack map_map. elim: s; [done | by case=> l /= ->]. Qed.
imports: Relation_Operators Lia PeanoNat List Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(Nat_facts List_facts Enumerable) Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.CM1_to_SMX ssreflect ssrbool ssrfun