Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Alph,S1,S2:. A1:Automata(Alph;S1). A2:Automata(Alph;S2). A1 A2

Applied Tactic: Unfold `refine` 0 THEN Auto
Generated subgoals:

None