proposition: Lemma not_alt_all {h} (ps : alt_option h valid0) : False.
proof: Proof. destruct ps as [ ? [ H' _ ] ]. revert H'; clear; intros [? ?]. congruence. Qed.
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