1. Id
2. Id
3. x : Id
4. A : Type
5. T : Type
6. P : ATProp
  (s,v. P(s(x),v))  State(x : A)TProp

By:	Repeat (Unfolds [`ma-state`;`fpf-single`;`fpf-cap`;`fpf-ap`;`fpf-dom`] 0 THEN Reduce 0) THEN DoSubsume THEN RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true 0 THEN Reduce 0 THEN Analyze 0

None

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