Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
T,P,z.
x
[].P[x])
T:
P:(T
)
True
Applied Tactic:
ProveOpCombTyping `list_all_wf_nil`
Generated subgoals:
None
(
T,P,z.
x
[].P[x]) T:
P:(T ) 
True