proposition: Fact mb_is_pair_inj p x y x' y' : p ≋ ⦃x,y⦄ -> p ≋ ⦃x',y'⦄ -> x ≈ x' /\ y ≈ y' \/ x ≈ y' /\ y ≈ x'.
proof: Proof. unfold mb_is_pair; intros H1 H2. generalize (proj1 (H2 x)) (proj1 (H2 y)); rewrite H1, H1, mb_equiv_refl_True, mb_equiv_refl_True. generalize (proj1 (H1 x')) (proj1 (H1 y')); rewrite H2, H2, mb_equiv_refl_True, mb_equiv_refl_True. intros [] [] [] []; 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)