proposition: Lemma rdp_list_production_tl_valid : forall p, rdp_list_production_carrier_valid p -> rdp_list_production_carrier_valid (rdp_list_production_tl p).
proof: Proof. unfold rdp_list_production_carrier_valid, default_production_carrier_valid, rdp_list_production_tl, default_production_tl; simpl; trivial. repeat match goal with | _ => progress simpl in * | _ => intro | _ => progress unfold is_true in * | [ |- andb ?x ?y = true ] => apply Bool.andb_true_iff | [ H : andb ?x ?y = true |- _ ] => apply Bool.andb_true_iff in H | [ H : and _ _ |- _ ] => destruct H | [ H : ?x = true |- context[?x] ] => rewrite H | [ |- ?x = ?x ] => reflexivity | [ |- and _ _ ] => split | [ |- context[if ?e then _ else _] ] => destruct e eqn:? end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Common.List.ListFacts