simp_all only [List.replicate, List.cons.injEq, true_and]
case cons.mpr.intro.succ
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
n✝ : Nat
h : c :: g = List.replicate (n✝ + 1) []
⊢ c = [] ∧ ∃ n, g = List.replicate n []
case cons.mpr.intro.succ
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
n✝ : Nat
ih : (∀ (x : Clause α✝), x ∈ List.replicate n✝ [] → x = []) ↔ ∃ n, List.replicate n✝ [] = List.replicate n []
h : c = [] ∧ g = List.replicate n✝ []
⊢ ∃ n, List.replicate n✝ [] = List.replicate n []