Formation

A universe intro rule such as `` >> by intro rec'' cannot be phrased easily in the refinement logic style because of the syntactic restriction on T in the extracted term rec(z,x.T;a) . One could give an approximate solution (as was done for set elim), but here we settle for no rule at all, thereby forcing the use of the explicit intro rule.

  .
  H,r:ind(z,x¯.T;a) >> Gagggggggby ind r over A 
 ¯[EXT foobar]¯[EXT foobar] H >>  rec(z,x.T;a)  in 
 				 by intro using A

z:A->
,x:A >> T in 

>> a in A