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