Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
P:T
.
L:T List.
x:T.
x
(x::L).P[x]
x
L.P[x]
Applied Tactic:
UnivCD THENA Auto
Generated subgoals:
1
.
x
L.P[x]
T:
. P:T 
. L:T List. x:T. x
(x::L).P[x] 
xL.P[x]xL.P[x]