IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq cons imp eq tls A:Type, a,b:A, as,bs:A List. a.as = b.bsas = bs
By:
RepD THEN (ApFunToHypEquands `z' tl(z) (A List) -1) THEN (Reduce -1)
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
A:Type, a,b:A, as,bs:A List. a.as = b.bs 
as = bs
