PrintForm Definitions finite sets Sections AutomataTheory Doc

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

Inj(n; n; Id)
By: Unfold `inject` 0
Generated subgoal:

1 a1,a2:n. Id(a1) = Id(a2) n a1 = a2

About:
natural_numberallimpliesequalapply