cases n
case cons.mpr.intro
α✝ : 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 []
⊢ c = [] ∧ ∃ n, g = List.replicate n []
case cons.mpr.intro.zero
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
h : c :: g = List.replicate 0 []
⊢ c = [] ∧ ∃ n, g = List.replicate n []

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 []