theorem DPDA_to_LR.activeHeadUnique_of_epsilonIntroducingHeadsUnique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hepsilon : EpsilonIntroducingHeadsUnique M) : ActiveHeadUnique M