PrintForm Definitions finite sets Sections AutomataTheory Doc

At: nsub is finite 1 1 1 1 2 1

1. n:

b:n. a:n. Id(a) = b

By: Reduce 0

Generated subgoal:

1 b:n. a:n. a = b


About:
allnatural_numberexistsequalapply