There are a number of solids, there are a number of very important classes of types, because this is a very rich structure language, I tell you that there is one which is inpredicative, that is going to the note propositions and there is another one which is going to the note data-types. They are essentially isomorphic, but of course we are distinguishing them because in proofs we want to distinguish what is a proof of a specification with respect to what is the algorithmic content of the proof. So, we are to take the first over the second according to the case.

---