induction x with
| nil => exact Or.inr ⟨0, rfl⟩
| cons c x ih => 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⟩
α : Type
x : CNF α
⊢ Nonempty α ∨ ∃ n, x = List.replicate n []
no goals