simp_all [ih]
case cons
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → List.isEmpty x = true) ↔ ∃ n, g = List.replicate n []
⊢ (∀ (x : Clause α✝), x ∈ c :: g → List.isEmpty x = true) ↔ ∃ n, c :: g = List.replicate n []
case cons
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
⊢ (c = [] ∧ ∃ n, g = List.replicate n []) ↔ ∃ n, c :: g = List.replicate n []