At:
sublist functionality wrt id list iso id T:Type, L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1(~eq1)L2 L3 = L4 (L1(eq2)L3 L2(eq2)L4)
By:
Analyze 0
THEN
Analyze 0
THEN
Analyze 0
THEN
Analyze 0
THEN
Equivalence -1
THEN
Analyze 0
THEN
Equivalence -1
THEN
UnivCD
Generated subgoal: