Nuprl - Proof: ma-single-pre1 wf

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

a:Id, T,A:Type, x:Id, P:(A

Prop).

ma-single-pre1(x;A;a;T;x,v.P(x,v))

MsgA

By:	Auto THEN Unfold `ma-single-pre1` 0 THEN Analyze THEN Try (Complete Auto) THEN Analyze THEN Try (Complete Auto) THEN GenConcl (s(x) = z) THEN Try (Complete Auto)

Generated subgoal:

1 1. Id
2. T : Type
3. A : Type
4. x : Id
5. ATProp
6. s : State(x : A)
s(x) A
2 steps

About:

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