rintro ⟨rfl, n, rfl⟩
case cons.mp
α✝ : 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 []
case cons.mp.intro.intro
α✝ : Type
n : Nat
ih : (∀ (x : Clause α✝), x ∈ List.replicate n [] → x = []) ↔ ∃ n_1, List.replicate n [] = List.replicate n_1 []
⊢ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []