A:Type, s:Sexpr(A). (x:A. s = Inj(x))  (s1,s2:Sexpr(A). s = Cons(s1;s2))

1

1. A : Type 2. s : Sexpr(A)   (x:A. s = Inj(x))  (s1,s2:Sexpr(A). s = Cons(s1;s2))

6 steps

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