PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin is decid 1 1 1 1 1 1 1 1 1 1 2
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: Unfold `decidable` 0
Generated subgoal:

1 x = y x = y

About:
equaluniversefunctionnatural_numberallimpliesapplyor