proposition: Fact env_vlift_fix0 φ n (v : vec X n) p : env_vlift φ v (pos2nat p) = vec_pos v p.
proof: Proof. revert φ p; induction v as [ | n x v IHv ]; intros phi p; auto. + invert pos p. + invert pos p. * rewrite pos2nat_fst; auto. * rewrite pos2nat_nxt; simpl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms) Undecidability.Shared.ListAutomation