ctx : Context
c : ExprCnstr
h : PolyCnstr.isValid (toNormPoly c) = true
this : PolyCnstr.denote ctx (toNormPoly c) = True
⊢ denote ctx c = True
ctx : Context
c : ExprCnstr
h : PolyCnstr.isValid (toNormPoly c) = true
⊢ denote ctx c = True
have := PolyCnstr.eq_true_of_isValid ctx h
ctx : Context
c : ExprCnstr
h : PolyCnstr.isValid (toNormPoly c) = true
this : denote ctx c = True
⊢ denote ctx c = True
ctx : Context
c : ExprCnstr
h : PolyCnstr.isValid (toNormPoly c) = true
this : PolyCnstr.denote ctx (toNormPoly c) = True
⊢ denote ctx c = True
simp at this
no goals
ctx : Context
c : ExprCnstr
h : PolyCnstr.isValid (toNormPoly c) = true
this : denote ctx c = True
⊢ denote ctx c = True
assumption