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. A1 A2

Conclusion:

|S1| |S2|

Applied Tactic: Unfold `connected` 6
Generated subgoals:

1. |S1| |S2|