PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
fun
enumer
1
1
2
1
1
1.
n:
Inj(
0
n;
(n
0);
z.0)
By:
Unfold `inject` 0
Generated subgoal:
1
a1,a2:(
0
n). (
z.0)(a1) = (
z.0)(a2)
(n
0)
a1 = a2
About:
a1,a2:(
0
n). (
z.0)(a1) = (z.0)(a2) 
(n
0) 
a1 = a2 Inj(0n; (n0); z.0) a1,a2:(0n). (z.0)(a1) = (z.0)(a2) (n0) a1 = a2
