Level: Lib Thy Top: 1
Hypotheses:

  1. A :

  2. A total

Conclusion:

Bot bar(A)

Applied Tactic: Unfold `bottom` 0
Generated subgoals:

1. Y (x.x) bar(A)