Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. l : Alph List

Conclusion:

(<St, l,s.Auto s l>:lI(Auto)) = Auto(l)

Applied Tactic: (ListInd 4 THEN RecUnfold `maction` 0 THENM RecUnfold `compute_list` 0 THENM Reduce 0 ...a)
Generated subgoals:

1. I(Auto) = I(Auto)

2. Auto (<St, l,s.Auto s l>:vI(Auto)) u = Auto Auto(v) u