Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph,St:
. Auto:Automata(Alph;St). MinAuto(Auto) 
Automata(Alph;x,y:(Alph List)//(x Rl y))
Applied Tactic: Unfold `min_auto` 0 THEN UnivCD THENA Auto
Generated subgoals:1. A(
l.Auto(l)
) Automata(Alph;x,y:(Alph List)//(x Rl y))