PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
enum
inj
q:
, l1,l2:
q*. enum(l1) = enum(l2)
l1 = l2
By:
UnivCD
Generated subgoal:
1
1.
q:
2.
l1:
q*
3.
l2:
q*
4.
enum(l1) = enum(l2)
l1 = l2
About:
q*q*
l1 = l2 
q:, l1,l2:q*. enum(l1) = enum(l2) 
l1 = l2q*q* l1 = l2
