. split <;> tauto;
case step.h_1
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
p✝ : Formula α
heq✝ : decode m✝ = some p✝
⊢ t[m].1 ⊆
    (if (𝓓)-Consistent (insert p✝ t[m✝].1, t[m✝].2) then (insert p✝ t[m✝].1, t[m✝].2)
      else (t[m✝].1, insert p✝ t[m✝].2)).1

case step.h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].1 ⊆ t[m✝].1
case step.h_2
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Inhabited α
inst✝ : Encodable α
t : Tableau α
m n m✝ : ℕ
h : m.le m✝
ih : t[m].1 ⊆ t[m✝].1
x✝ : Option (Formula α)
heq✝ : decode m✝ = none
⊢ t[m].1 ⊆ t[m✝].1