simp only [exists_and_left, ne_eq, Bool.forall_bool, Bool.not_eq_false, cond_false,
  Bool.not_eq_true, cond_true, inter_self, IsEmpty.forall_iff, forall_true_left, true_and,
  and_true]
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
⊢ ((∃ I J, M.Basis I X ∧ M.Basis J Y ∧ M.Indep (I ∪ J)) ∧
      ∀ ⦃i j : Bool⦄, i ≠ j → (fun i => bif i then X else Y) i ∩ (fun i => bif i then X else Y) j ⊆ M.cl ∅) ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X✝ X' Y✝ Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
X Y : Set α
⊢ (∃ I, M.Basis I X ∧ ∃ x, M.Basis x Y ∧ M.Indep (I ∪ x)) ∧ Y ∩ X ⊆ M.cl ∅ ∧ X ∩ Y ⊆ M.cl ∅ ↔
    ∃ I J, M.Indep (I ∪ J) ∧ Disjoint I J ∧ M.Basis I X ∧ M.Basis J Y