At:
disjoint iff assert disjoint21222
1.
T: Type
2.
eq: {T}
3.
eq TT
4.
L: T List
5.
M: T List
6.
u: T
7.
v: T List
8.
disjoint(eq;v;M) disjoint(eq;v;M)
9.
disjoint(eq;v;M) disjoint(eq;v;M)
10.
u(eq) M = false
11.
disjoint(eq;v;M)
disjoint(eq;v;M)
By:
HypBackchain
THEN
Trivial
Generated subgoals:
}
T
T
disjoint
disjoint(eq;v;M)