Nuprl - Proof: fpf-val-single1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-val-single1 2

1. A : Type
2. eq : EqDecider(A)
3. x : A
4. v : Top
5. P : Top

((true

false

)

P(x,<[x],

x.v>(x))) ~ (True

P(x,v))

By:	Unfold `fpf-ap` 0 THEN Reduce 0

Generated subgoals:

None

About:

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