proposition: Lemma invert_full_productions_carrierT_reachableT p ps (H : full_productions_carrierT_reachableT (p::ps)) : (full_production_carrierT_reachableT p * full_productions_carrierT_reachableT ps)%type.
proof: Proof. destruct H as [nt [prefix [H0 H1]]]; split; exists nt; [ exists 0; exists p; simpl; repeat split; try assumption | exists (prefix ++ [p]); rewrite <- app_assoc; simpl; split; assumption ]. rewrite <- H1. clear. induction prefix; simpl in *; [ left | right ]; trivial. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Arith.EqNat Coq.Arith.Compare_dec Coq.Arith.Wf_nat Coq.ZArith.ZArith Fiat.Common.List.Operations Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericCorrectnessBaseTypes Fiat.Parsers.StringLike.Properties Fiat.Parsers.MinimalParse Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.WellFoundedParse Fiat.Parsers.MinimalParseOfParse Fiat.Parsers.GenericRecognizer Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf Fiat.Common.Wf1 Fiat.Common.List.ListFacts Fiat.Common.NatFacts Fiat.Common.UIP Fiat.Common