Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
n,m:
.
f:(
n
m)
(n * m). Bij(
n
m;
(n * m);f)
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
.
f:(
n
m)
(n * m). Bij(
n
m;
(n * m);f)
n,m:
. 
f:(n 
m) 
(n * m). Bij(n m;(n * m);f)f:(n m) (n * m). Bij(n m;(n * m);f)