proposition: Lemma encode_list_app (xs ys : list X) : encode_list (xs ++ ys) = removelast (encode_list xs) ++ encode_list ys.
proof: Proof. revert ys. induction xs; intros; cbn in *; f_equal. rewrite IHxs. rewrite app_assoc, app_comm_cons; f_equal. destruct (map (fun x : sigX => sigList_X x) (encode a)) eqn:E; cbn. - destruct xs; cbn; auto. - f_equal. destruct (encode a) eqn:E2; cbn in E. { congruence. } rewrite removelast_app. + destruct (l ++ encode_list xs) eqn:E3; cbn; auto. apply app_eq_nil in E3 as (E3&E3'). destruct xs; inv E3'. + destruct xs; cbn; congruence. Qed.
imports: Undecidability(TM.Util.Prelim) Coq.Lists.List