PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
list
1
1
nat
1
1
1
1.
q:
Bij(
q*;
;
l.enum(l))
By:
UnfoldTopAb 0
THEN
Analyze 0
THEN
UnfoldTopAb 0
THEN
Reduce 0
Generated subgoals:
1
a1,a2:
q*. enum(a1) = enum(a2)
a1 = a2
2
b:
.
a:
q*. enum(a) = b
About:
a1,a2:
q*. enum(a1) = enum(a2) 
a1 = a2 b:. 
a:q*. enum(a) = b
Bij(q*; ; 
l.enum(l)) a1,a2:q*. enum(a1) = enum(a2) a1 = a2 b:. a:q*. enum(a) = b
