Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
T,eq,u,z.u(
eq) [])
T:
eq:(T
T
)
u:T
True
Applied Tactic:
ProveOpCombTyping `is_member_wf_nil`
Generated subgoals:
None
(
T,eq,u,z.u(
eq) []) T:
eq:(T T 
) u:T 
True