proposition: Fact Σ2_is_tuple_in_vars r n v : fol_vars (@Σ2_is_tuple_in r n v) ⊑ r::vec_list v.
proof: Proof. unfold Σ2_is_tuple_in. intros x; rewrite fol_vars_quant, in_flat_map. intros (y & H1 & H2). rewrite fol_vars_bin, in_app_iff in H1. destruct H1 as [ H1 | H1 ]. + apply Σ2_is_tuple_vars in H1. simpl in H1; rewrite vec_list_vec_map, in_map_iff in H1. destruct H1 as [ <- | (z & <- & H1) ]; simpl in *; try tauto. destruct H2 as [ <- | [] ]; auto. + simpl in H1. destruct H1 as [ <- | [ <- | [] ] ]; simpl in *; 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)