PrintForm Definitions finite sets Sections AutomataTheory Doc

At: prod fin is fin 1 1 1
1. T: Type
2. t: T
3. n:
4. f: nT
5. Bij(n; T; f)

n = 0
By:
Analyze 0
THEN
Unfold `biject` -2
Generated subgoal:

15. Inj(n; T; f) & Surj(n; T; f)
6. n = 0
False

About:
equalintnatural_numberuniversefunctionfalse