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