Level:
Lib
Thy
Top
:
1
1
Hypotheses:
None
Conclusion:
f:
2
. Bij(
2;
;f)
Applied Tactic:
With
n.if (n =
0) then tt else ff fi
(D 0) THENW Auto
Generated subgoals:
1
. Bij(
2;
;
n.if (n =
0) then tt else ff fi )
f:
2 
. Bij(2;;f)
n.if (n =
0) then tt else ff fi 
(D 0) THENW Auto2;;n.if (n = 0) then tt else ff fi )