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