proposition: Fact mb_is_tuple_congr p q n (v : vec X n) : p ≈ q -> p ≋ ⦉v⦊ -> q ≋ ⦉v⦊ .
proof: Proof. Proof using mb_axiom_ext. revert p q; induction v as [ | n x v IHv ]; intros p q. + simpl; intros E H x; rewrite <- E; auto. + intros E (t & H1 & H2); exists t; split; auto. rewrite <- E; auto. 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)