rintro rfl
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
C : Set α
hC : C.Nonempty
D : Set α
⊢ D = C → (D ⊆ C → D = C) ∧ D ⊆ C
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
D : Set α
hC : D.Nonempty
⊢ (D ⊆ D → D = D) ∧ D ⊆ D