Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
. L1,L2:T List. eq1,eq2,eq3:{T
}. L3,L4:T List.
Discrete{T} 
eq1 = eq2 eq2 = eq3 L1(
eq1)L2 L3(eq2)L4 {(L1 @ L3)(eq3)(L2 @ L4)}
Applied Tactic: RepeatFor 3 (D 0 THENA Auto) THEN
RepeatFor 3 (D 0 THENA Auto THEN Equivalence (-1)) THEN
UnivCD THENA Auto
Generated subgoals:1. (L1 @ L3)(eq3)(L2 @ L4)