proposition: Lemma pull_If_bool {R R' rn rc} {b : bool} (f : R -> R') : (If b Then f rn Else f rc) = f (If b Then rn Else rc).
proof: Proof. destruct b; reflexivity. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.StringLike.FirstCharSuchThat Coq.Strings.String Coq.Arith.PeanoNat Fiat.Computation.Core Coq.Program.Program Fiat.Computation.ApplyMonad Fiat.Computation.SetoidMorphisms Fiat.Common Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common.Equality Fiat.Common.BoolFacts Fiat.Common.NatFacts Coq.Lists.List