PrintForm Definitions finite sets Sections AutomataTheory Doc

At: nsub is finite 1 1 1 1 1 1
1. n:

a1,a2:n. Id(a1) = Id(a2) n a1 = a2
By: Reduce 0
Generated subgoal:

1 a1,a2:n. a1 = a2 a1 = a2

About:
allnatural_numberimpliesequalapply