Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,S1,S2:
. A1:Automata(Alph;S1). A2:Automata(Alph;S2). A1 
A2 
A2 A1
Applied Tactic: Unfold `auto_iso` 0 THEN Auto
Generated subgoals:1. 
f:S2 
S1
Bij(S2;S1;f)
(s:S2. a:Alph. f (
A2 s a) = A1 (f s) a)
f I(A2) = I(A1)
(s:S2. F(A2) s = F(A1) (f s))