PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin is decid 1 1 1 1 1 1 1 1 1 1 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. x = y

x = y x = y
By: Sel 1 (Analyze 0)
Generated subgoals:

None

About:
orequaluniversefunctionnatural_numberallimpliesapply