Level: Lib Thy Top: 1 1
Hypotheses:

  1. T :

  2. n :

  3. f:n T. Bij(n;T;f)

  4. x : T

  5. y : T

Conclusion:

Dec(x = y)

Applied Tactic: D 3
Generated subgoals:

1. Dec(x = y)