Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
eq:{T
}.
x:T.
L:T List.
x(
eq) L
(
y:T.
x(
eq) (y::L))
Applied Tactic:
RepeatFor 2 (D 0 THENA Auto) THEN Equivalence (-1) THEN UnivCD THENA Auto
Generated subgoals:
1
.
x(
eq) (y::L)
T:
. eq:{T
}. x:T. L:T List. 
x(
eq) L 
(y:T. x(eq) (y::L))x(eq) (y::L)