PrintForm Definitions finite sets Sections AutomataTheory Doc

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

Dec(x = y)
By: ApFunToHypEquands `i' (f(i)) T 11
Generated subgoal:

112. f(a) = f(a1)
Dec(x = y)

About:
equalapplyuniversefunctionnatural_numberallimplies