Nuprl - Proof: htype definition wd 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: htype definition wd 1

1. 'b : S
2. 'a : S
3. P : 'a

4. rep : 'b

(

type_definition('a;'b;P;rep))

((

x',x'':'b. ((rep(x')) =

(rep(x'')))

(x' =

x''))

((

x:'a. ((P(x)) =

(

x':'b. (x =

(rep(x')))))))

By:	Unab [`type_definition`] THEN Simpsetp [`bequal`] THEN StrongAuto THEN Try HypBackchain THEN StrongAuto

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html