Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
P:T
.
x
[].P[x]
Applied Tactic:
Rewrite (HigherC list_all_unrollC) 0 THEN Auto
Generated subgoals:
None
T:
. P:T 
. x
[].P[x]