proposition: Lemma rdp_list_remove_nonterminal_1 : forall ls ps ps', rdp_list_is_valid_nonterminal (rdp_list_remove_nonterminal ls ps) ps' = true -> rdp_list_is_valid_nonterminal ls ps' = true.
proof: Proof. unfold rdp_list_is_valid_nonterminal, rdp_list_remove_nonterminal. fix_eqs. repeat match goal with | _ => exfalso; congruence | _ => reflexivity | _ => assumption | [ |- context[if ?E then _ else _] ] => destruct E | _ => intro | [ H : In _ (filter _ _) |- _ ] => apply filter_In in H | [ H : _ /\ _ |- _ ] => destruct H | [ H : ?T, H' : ~?T |- _ ] => destruct (H' H) | [ H : list_bin _ _ _ = true |- _ ] => apply list_in_bl in H; [ | solve [ intros; apply (fun n m => (proj1 (Nat.eqb_eq n m))); trivial ] ] | [ |- list_bin _ _ _ = true ] => apply list_in_lb | _ => progress subst | [ |- context[Nat.eqb ?x ?x] ] => rewrite Nat.eqb_refl 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