fact: Fixpoint transfer_forall_parse_of str1 str2 pats (HR : R str1 str2) {p} {struct p} : @Forall_parse_of Char _ HSL1 G (fun _ => P) str1 pats p -> @Forall_parse_of Char _ HSL2 G (fun _ => P) str2 pats (transfer_parse_of HR p) := match p in (parse_of _ _ pats) return (@Forall_parse_of Char _ HSL1 G (fun _ => P) str1 pats p -> @Forall_parse_of Char _ HSL2 G (fun _ => P) str2 pats (transfer_parse_of HR p)) with | ParseHead _ _ p' => @transfer_forall_parse_of_production _ _ _ _ p' | ParseTail _ _ p' => @transfer_forall_parse_of _ _ _ _ p' end with transfer_forall_parse_of_production str1 str2 pat (HR : R str1 str2) {p} {struct p} : @Forall_parse_of_production Char _ HSL1 G (fun _ => P) str1 pat p -> @Forall_parse_of_production Char _ HSL2 G (fun _ => P) str2 pat (transfer_parse_of_production HR p) := match p in (parse_of_production _ _ pat) return (@Forall_parse_of_production Char _ HSL1 G (fun _ => P) str1 pat p -> @Forall_parse_of_production Char _ HSL2 G (fun _ => P) str2 pat (transfer_parse_of_production HR p)) with | ParseProductionNil _ => fun x => x | ParseProductionCons _ _ _ p0 p1 => fun xy => (@transfer_forall_parse_of_item' (@transfer_forall_parse_of) _ _ _ _ p0 (fst xy), @transfer_forall_parse_of_production _ _ _ _ p1 (snd xy)) end.
imports: Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.Transfer