Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
A:
. A total
(
a:bar(A). (a in! A)
)
Applied Tactic:
Auto
Generated subgoals:
None
A:
. A total 
(a:bar(A). (a in! A) 
)