In pairs mode, we now interpret

     Axiom 3.4.21 pi { ⊢ T Type } { t : T ⊢ U Type } ⊢ [∏;t](T,U/t) Type .

as

     pi : (t:(T:texp) ⟶ (U:oexp ⟶ texp) ⟶ Singleton(([∏] T (t1 ⟼ (U t1))) : texp)) ×
          (T:(T1:texp) × istype T1) ⟶
	  (U:(U1:oexp ⟶ texp) × (t1:(t2:oexp) × hastype t2 T₁) ⟶ (U2:Singleton((U1 t1₁) : texp)) × istype U2) ⟶
	  (t1:Singleton((t T₁ U₁) : texp)) × istype t1)

.  The hope was that by having pi_2 return a pair of type (t1:Singleton((t T₁ U₁) : texp)) × istype t1),
the result would be shorter proofs.  Look in test3.ts for a proof of modus_ponens in pairs mode, still
not as short as desired.  Can it be shortened further?