fact: Fixpoint maybe_empty_productions__of__minimal_maybe_empty_productions {valid0} valid pats (Hsub : sub_nonterminals_listT valid valid0) (H : minimal_maybe_empty_productions (G := G) valid pats) : maybe_empty_productions G valid0 pats with maybe_empty_production__of__minimal_maybe_empty_production {valid0} valid pat (Hsub : sub_nonterminals_listT valid valid0) (H : minimal_maybe_empty_production (G := G) valid pat) : maybe_empty_production G valid0 pat.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.Reachable.MaybeEmpty.Core Fiat.Parsers.Reachable.MaybeEmpty.Minimal Fiat.Parsers.BaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.Reachable.MaybeEmpty.WellFounded Fiat.Common