Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
t:
.
n:
. #(t)=n
Applied Tactic:
(Unfold `card` 0 ...)
Generated subgoals:
None
t:
. n:
. #(t)=n 
