proposition: Fact mb_is_tuple_fun p q n (v : vec _ n) : p ≋ ⦉v⦊ -> q ≋ ⦉v⦊ -> p ≈ q.
proof: Proof. Proof using mb_axiom_ext. revert p q; induction v as [ | n x v IHv ]; intros p q. + simpl; intros H1 H2. apply mb_equiv_eq; split. * intros z Hz; apply H1 in Hz; tauto. * intros z Hz; apply H2 in Hz; tauto. + intros (p' & H1 & H2) (q' & H3 & H4). generalize (IHv _ _ H2 H4); intros E. rewrite E in H1. revert H1 H3; apply mb_is_opair_fun. 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)