proposition: Fact Σ2_is_tuple_spec t n v ψ : ⟪@Σ2_is_tuple t n v⟫ ψ <-> mb_is_tuple mem (ψ t) (vec_map ψ v).
proof: Proof. induction n as [ | n IHn ] in t, v, ψ |- *. + vec nil v; reflexivity. + vec split v with x. simpl Σ2_is_tuple. simpl mb_is_tuple. rewrite fol_sem_quant_fix. fol equiv ex; intros y. rewrite fol_sem_bin_fix. fol equiv conj. * reflexivity. * rewrite IHn, vec_map_map; reflexivity. 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)