Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. S1 :

  3. S2 :

  4. A1 : Automata(Alph;S1)

  5. A2 : Automata(Alph;S2)

  6. L(A1) = L(A2)

Conclusion:

x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rl y)

Applied Tactic: InstLemma `lang_rel_equi` [Alph;L(A1)] THENA Auto THEN InstLemma `lang_rel_equi` [Alph;L(A2)] THENA Auto
Generated subgoals:

1. x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rl y)