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