exact ⟨_, rfl⟩
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 []
no goals