dsimp [relabelFin]
g : CNF Nat
⊢ g.relabelFin.unsat ↔ g.unsat
g : CNF Nat
⊢ (if h : ∃ a, mem a g then relabel (fun i => if w : i < g.numLiterals then ⟨i, w⟩ else ⟨0, ⋯⟩) g
      else List.replicate (List.length g) []).unsat ↔
    g.unsat