Definitions
array
1
Doc
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
T:Type, i:
, j:{i...}, a:[T]Array{i..j
}. a.l = i & a.u = j