PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin is decid 1 1 1 1 1 1 1 1 1 1 2 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

x = y x = y
By: Sel 2 (Analyze 0)
Generated subgoal:

1 x = y

About:
orequaluniversefunctionnatural_numberallimpliesapply