Level: Lib Thy Top: 1 2
Hypotheses:

  1. T :

  2. t : T

  3. n :

  4. f : n T

  5. Bij(n;T;f)

  6. n > 0

Conclusion:

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

Applied Tactic: (InstConcl [n * n;x.<f (x n), f (x rem n)>] ...a)
Generated subgoals:

1. 0 n * n

2. 0 x n

3. x n < n

4. 0 x rem n

5. x rem n < n

6. Bij((n * n);T T;x.<f (x n), f (x rem n)>)