IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
p array properties T:Type, i:, j:{i...}, a:[T]Array{i..j}. a.l = i & a.u = j
By:
ProvePropertiesLemma
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
T:Type, i:
, j:{i...}, a:[T]Array{i..j
}. a.l = i & a.u = j
