To be only a little more precise, every proposition becomes a type of its own. The AND operator forms product types, the OR operator forms sum types, IMPLIES forms a function type... The proof of a theorem turns into an inhabitant of the theorem's type.