proposition: Lemma eval_L_from n p L : eval (@conv n p) (L_from (fun p : pos n => nth (pos2nat p) L 0)) = eval (conv p) L.
proof: Proof. induction p; cbn. - reflexivity. - revert L; induction n; intros; cbn. + invert pos v. + invert pos v. * rewrite pos2nat_fst. reflexivity. * rewrite pos2nat_nxt in *. destruct L. -- cbn. clear. induction n. ++ cbn. invert pos v. ++ cbn. invert pos v. rewrite !pos.pos2nat_fst. now rewrite pos.pos2nat_nxt. now rewrite pos.pos2nat_nxt. -- cbn. now rewrite <- IHn with (L := L). - invert pos p. - destruct d; cbn; congruence. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.PCP.Util.PCP_facts Undecidability.Shared.Libs.PSL.FiniteTypes Undecidability.L.Datatypes(LNat LProd) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared.Libs.DLW.Vec(pos) Undecidability.L.Datatypes.List(List_basics List_extra) Nat Datatypes