proposition: Fact Σ2_is_tuple_vars t n v : fol_vars (@Σ2_is_tuple t n v) ⊑ t::vec_list v.
proof: Proof. revert t v; induction n as [ | n IHn ]; intros t v. + vec nil v; cbv; tauto. + vec split v with x; simpl Σ2_is_tuple. intros i; rewrite fol_vars_quant, in_flat_map. intros (j & H1 & H2). rewrite fol_vars_bin, in_app_iff in H1. destruct H1 as [ H1 | H1 ]. * apply Σ2_is_opair_vars in H1. destruct H1 as [ | [ | [ | [] ] ] ]; subst j; simpl in *; tauto. * apply IHn in H1. destruct H1 as [ <- | H1 ]. - simpl in *; tauto. - rewrite vec_list_vec_map, in_map_iff in H1. destruct H1 as (y & <- & H1); simpl in *. destruct H2 as [ -> | [] ]; tauto. Qed.
imports: List Arith Nat Lia Max Wellfounded Coq.Setoids.Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations fol_ops fo_sig fo_terms fo_logic)