IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
es-after-pred es:ES, x:Id, e:E.
first(e) (x after pred(e)) = (x when e) vartype(loc(e);x)
By:
Use_ES_Axioms THEN Symmetry THEN BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
es:ES, x:Id, e:E.
first(e) 
(x after pred(e)) = (x when e) 
vartype(loc(e);x)
