fact: Fixpoint encode_list (xs : list X) : list (sigList sigX) := match xs with | nil => [sigList_nil] | x :: xs' => sigList_cons :: (map sigList_X (encode x)) ++ encode_list xs' end.
imports: Undecidability(TM.Util.Prelim) Coq.Lists.List