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