rw [← AIG.toCNF_equisat]
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ bv.bitblast.relabelNat.unsat
case a
bv : BVLogicalExpr
c : LratCert
h : verifyBVExpr bv c = true
⊢ (AIG.toCNF bv.bitblast.relabelNat).unsat