next up previous contents index
Next: Intro Up: Inductive Type Proof Previous: Inductive Type Proof


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

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995