ctx : Context
c : ExprCnstr
h : PolyCnstr.isUnsat (toNormPoly c) = true
this : PolyCnstr.denote ctx (toNormPoly c) = False
⊢ denote ctx c = False
ctx : Context
c : ExprCnstr
h : PolyCnstr.isUnsat (toNormPoly c) = true
⊢ denote ctx c = False
have := PolyCnstr.eq_false_of_isUnsat ctx h
ctx : Context
c : ExprCnstr
h : PolyCnstr.isUnsat (toNormPoly c) = true
this : denote ctx c = False
⊢ denote ctx c = False
ctx : Context
c : ExprCnstr
h : PolyCnstr.isUnsat (toNormPoly c) = true
this : PolyCnstr.denote ctx (toNormPoly c) = False
⊢ denote ctx c = False
simp at this
no goals
ctx : Context
c : ExprCnstr
h : PolyCnstr.isUnsat (toNormPoly c) = true
this : denote ctx c = False
⊢ denote ctx c = False
assumption