improve the default tactic so it works in a hole whose type is
that of a constant function
In pairs mode,

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

was getting realized as

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

, but now we've changed it to this:

	(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₁) ⟶ istype (U1 t1₁)) ⟶
	istype (t T₁ U₁)

Thus each theorem now returns an expression and a typing judgment about it, which
is appropriate, since premisses of inference rules expect such pairs.