proposition: Fact mb_is_opair_inj p x y x' y' : p ≋ ⦅x,y⦆ -> p ≋ ⦅x',y'⦆ -> x ≈ x' /\ y ≈ y'.
proof: Proof. Proof using mb_axiom_ext. intros (a & b & H1 & H2 & H3) (u & v & G1 & G2 & G3). generalize (mb_is_pair_inj H3 G3); intros [ (E1 & E2) | (E1 & E2) ]. + rewrite E1 in H1; rewrite E2 in H2. generalize (mb_is_pair_inj' H1 G1); intros E; split; auto. rewrite E in H2. generalize (mb_is_pair_inj H2 G2); intros [ | (E3 & E4) ]; try tauto. rewrite E4; auto. + rewrite E1 in H1; rewrite E2 in H2. generalize (mb_is_pair_inj H2 G1) (mb_is_pair_inj H1 G2). intros [ (E3 & E4) | (E3 & E4) ] [ (E5 & E6) | (E5 & E6) ]; rewrite E4, <- E5; 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)