match c with
| [] => cases ih with
| inl h => left; exact h
| inr h =>
obtain ⟨n, rfl⟩ := h
right
exact ⟨n + 1, rfl⟩
| ⟨a, b⟩ :: c => exact Or.inl ⟨a⟩
case cons
α : Type
c : Clause α
x : List (Clause α)
ih : Nonempty α ∨ ∃ n, x = List.replicate n []
⊢ Nonempty α ∨ ∃ n, c :: x = List.replicate n []
no goals