Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Alph,St:. Auto:Automata(Alph;St). l:x,y:(Alph List)//(Auto(x) = Auto(y)). Auto(l) St

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

1. Auto(l) St

2. EquivRel(Alph List;x,y.Auto(x) = Auto(y))