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