refine Finset.insert_subset_iff.mpr ?_
case h
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
h✝ : φ = φ' ∧ ψ = ψ'
⊢ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))
case h
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
h✝ : φ = φ' ∧ ψ = ψ'
⊢ φ ∈ insert φ' (insert ψ' (L.erase (φ'⋀ψ'))) ∧ {ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))