Nuprl - Proof: w-val wf

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-val wf

the_w:World, i:Id, a:Action(i).

isnull(a)

val(a)

valtype(i;a)

By:	Auto THEN Unfold_Wld 1 THEN Analyze -2 THEN Analyze -2 THEN All Reduce THEN DoSubsume THEN Unfold `w-action-dec` 0 THEN KindCase -3 THEN SplitOnConclITE THEN At Type (Analyze 0)

Generated subgoals:

None

About:

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