Definitions
array
1
Doc
At:
array
append
wf
1
1
1.
T:
Type
2.
i:
3.
j:
{i...}
4.
k:
{j...}
5.
a:
[T]Array
6.
a.l = i
7.
a.u = j
8.
b:
[T]Array
9.
b.l = j
10.
b.u = k
a @ b
[T]Array{i..k
}
By:
AbSetMemEqTypeCD
Generated subgoals:
1
a @ b
[T]Array
2
a @ b.l = i & a @ b.u = k
a @ b.l = i & a @ b.u = k