Nuprl - Proof: ma-single-pre1 wf 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-single-pre1 wf 1 1

1. Id
2. T : Type
3. A : Type
4. x : Id
5. A

Prop
6. x@0:Id

if eqof(IdDeq)(x,x@0)

false

A else Top fi

if eqof(IdDeq)(x,x)

false

A else Top fi

r A

By:	((RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true 0) THEN (Reduce 0)) THEN Analyze 0

Generated subgoals:

None

About:

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