|
|
|---|
|
|
|
|---|
Fixtype of proof obligations.
This is a product type introduced by fty::defprod.
These are the proof obligations that arise from expressions.
A proof obligation consists of a list of typed variables, a list of hypotheses, and a conclusion. One can form a formula from it, universally quantified over the variables, where each hypothesis becomes an implication antecedent (when it is an expression) or a let binding (when it is a binding),, and where the conclusion becomes the final implication consequent or let binding body. This formula construction will be defined later.