PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
list
1
1
nat
1
1
1
1
1
1.
q:
2.
a1:
q*
3.
a2:
q*
4.
enum(a1) = enum(a2)
a1 = a2
By:
BackThru
Thm*
q:
, l1,l2:
q*. enum(l1) = enum(l2)
l1 = l2
Generated subgoals:
None
About:
q*q*
a1 = a2
q:, l1,l2:q*. enum(l1) = enum(l2) 
l1 = l2
