Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
T,z.Fin(T))
T:
True
Applied Tactic:
ProveOpCombTyping `finite_wf`
Generated subgoals:
None