PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin is decid 1 1

1. T: Type
2. n:
3. f:(nT). Bij(n; T; f)
4. x: T
5. y: T

Dec(x = y)

By: Analyze 3

Generated subgoal:

13. f: nT
4. Bij(n; T; f)
5. x: T
6. y: T
Dec(x = y)


About:
equaluniverseexistsfunctionnatural_number