//------------------------------------------------------------------------------------
// Natural Numbers
//   The type "nat::forall<X, Prop>" is a proposition.
//   To create an instance (= proof) of the propotision,
//   you must supply

//------------------------------------------------------------------------------------
// [Metafunction] Substitution as usual
//------------------------------------------------------------------------------------