cases n with
| zero => simp at h
| succ n =>
  simp_all
case isFalse.cons.intro
c : Clause Nat
g : List (Clause Nat)
n : Nat
h : c :: g = List.replicate n []
⊢ unsat (List.replicate (c :: g).length []) ↔ unsat (c :: g)
no goals