Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Alph,St:. Auto:Automata(Alph;St). x,y,z:Alph List. Auto(x) = Auto(y) Auto(z @ x) = Auto(z @ y)

Applied Tactic: GenUnivCD THENW Auto
Generated subgoals:

1. Auto(z @ x) = Auto(z @ y)