Add support for realizability-based extraction

The *proof term* for `Π(Zero = One) Zero` is `λp. reflect p in tt`. But
the *computational realizer* for that sentence in Type Theory is just
`λp. tt`.

A value (u :||- φ) type "Realization" should be considered a witness
that the term u realizes the sentence φ.