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