PrintForm Definitions finite sets Sections AutomataTheory Doc

At: prod fin is fin 1 1 1 1 1
1. T: Type
2. t: T
3. n:
4. f: nT
5. Inj(n; T; f)
6. b:T. a:n. f(a) = b
7. n = 0

False
By:
InstHyp [t] -2
THEN
Analyze -1
Generated subgoals:

None

About:
falseuniversefunctionnatural_numberall
existsequalapplyint