rw [← AIG.Entrypoint.relabelNat_unsat_iff]
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.unsat
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.relabelNat.unsat