proposition: Lemma encode_list_remove (xs : list X) : removelast (encode_list xs) ++ [sigList_nil] = encode_list xs.
proof: Proof. induction xs. - reflexivity. - cbn [encode_list]. change (sigList_cons :: map sigList_X (encode a) ++ encode_list xs) with ((sigList_cons :: map sigList_X (encode a)) ++ encode_list xs). rewrite removelast_app by apply encode_list_neq_nil. rewrite <- app_assoc. f_equal. auto. Qed.
imports: Undecidability(TM.Util.Prelim) Coq.Lists.List