Nuprl Basics - Proof: sfa doc sexprcarsize 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc sexprcarsize 1 1 2

1. A : Type
2. Q : Sexpr(A)

Prop
3.

s:{s:Sexpr(A)| Q(s) }. Size(s)

Size(sexprCar(s))<Size(s)
4. y : A
5. Size(Inj(y))

Size(sexprCar(Inj(y)))<Size(Inj(y))

By:	Compute-1 Size(Inj(y)) * 1

Generated subgoals:

None

About:

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