PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin is decid 1 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1
1. T: Type
2. n:
3. f: nT
4. a1,a2:n. f(a1) = f(a2) a1 = a2
5. x: T
6. y: T
7. a: n
8. f(a) = x
9. a1: n
10. f(a1) = y
11. a = a1
12. f(a) = f(a1)

False
By: InstHyp [a;a1] 4
Generated subgoals:

None

About:
falseuniversefunctionnatural_numberallimpliesequalapply