Level:
Lib
Thy
Top
:
1
Hypotheses:
Alph :
St :
Auto : Automata(Alph;St)
Fin(Alph)
Fin(St)
x : Alph List
y : Alph List
Conclusion:
Dec(x = y)
Applied Tactic:
InstLemma `mn_13` [
Alph
;
St
;
Auto
] THENA Auto
Generated subgoals:
1
. Dec(x = y)