apply not_mem₂_iff_mem₁ ct₁ |>.mp
case mpr.a
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
h : t₁.2 = t₂.2
p : Formula α
hp : p ∈ t₂.1
⊢ p ∈ t₁.1
case mpr.a
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : autoParam ((𝓓)-Consistent t) _auto✝
hMat : autoParam t.Saturated _auto✝
t₁ t₂ : Tableau α
ct₁ : (𝓓)-Consistent t₁
ct₂ : (𝓓)-Consistent t₂
st₁ : t₁.Saturated
st₂ : t₂.Saturated
h : t₁.2 = t₂.2
p : Formula α
hp : p ∈ t₂.1
⊢ p ∉ t₁.2