simp_all
case mk.mk
cnf : CNF Nat
h2 : cnf.lift.unsat
val✝¹ : Nat
isLt✝¹ : val✝¹ < cnf.numLiterals
ha : mem ⟨val✝¹, isLt✝¹⟩ cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
hb : mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ ⟨val✝¹, isLt✝¹⟩ = ⟨val✝, isLt✝⟩
no goals