Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. S1 :

  3. S2 :

  4. A1 : Automata(Alph;S1)

  5. A2 : Automata(Alph;S2)

  6. Con(A1)

  7. Con(A2)

  8. L(A1) = L(A2)

  9. A1 A2

  10. A2 A1

Conclusion:

A1 A2

Applied Tactic: Unfold `connected` 6
Generated subgoals:

1. A1 A2