PrintForm Definitions finite sets Sections AutomataTheory Doc

At: fin is decid

T:Type. Fin(T) (x,y:T. Dec(x = y))
By: UnivCD
Generated subgoal:

11. T: Type
2. Fin(T)
3. x: T
4. y: T
Dec(x = y)

About:
alluniverseimpliesequal