Level: Lib Thy Top: 1 1
Hypotheses:

  1. A :

  2. A total

Conclusion:

Y (x.x) bar(A)

Applied Tactic: Unfold `member` 0
Generated subgoals:

1. Y (x.x) = Y (x.x)