propositions-as-types Some scribbling while reading Type Theory and Formal Proofs by Rob Nederpelt and Herman Geuvers