have h3 :=
  CNF.unsat_relabel_iff
    (by
      intro a b ha hb hab
      injections hab
      cases a; cases b; simp_all)
    |>.mp h2
cnf : CNF Nat
h2 : cnf.lift.unsat
⊢ cnf.unsat
cnf : CNF Nat
h2 : cnf.lift.unsat
h3 : cnf.relabelFin.unsat
⊢ cnf.unsat