Level:
Lib
Thy
Top
:
1
Hypotheses:
None
Conclusion:
Fin(x,y:(
1 List)//(x Rl y))
Applied Tactic:
BLemma `mn_13` THENA Auto THEN D 0 THEN BLemma `nsub_is_finite` THEN Auto
Generated subgoals:
None
Fin(x,y:(
1 List)//(x Rl y))