fact: Definition transfer_forall_parse_of_item' (transfer_forall_parse_of : forall str1 str2 it (HR : R str1 str2) p, @Forall_parse_of Char _ _ G (fun _ => P) str1 it p -> @Forall_parse_of Char _ _ G (fun _ => P) str2 it (transfer_parse_of HR p)) {str1 str2 it} (HR : R str1 str2) {p} : @Forall_parse_of_item' Char _ HSL1 G (fun _ => P) (@Forall_parse_of _ _ _ _ (fun _ => P)) str1 it p -> @Forall_parse_of_item' Char _ HSL2 G (fun _ => P) (@Forall_parse_of _ _ _ _ (fun _ => P)) str2 it (transfer_parse_of_item HR p) := match p in (parse_of_item _ _ it) return (@Forall_parse_of_item' Char _ HSL1 G (fun _ => P) (@Forall_parse_of _ _ _ _ (fun _ => P)) str1 it p -> @Forall_parse_of_item' Char _ HSL2 G (fun _ => P) (@Forall_parse_of _ _ _ _ (fun _ => P)) str2 it (transfer_parse_of_item HR p)) with | ParseTerminal _ _ _ _ => fun x => x | ParseNonTerminal _ H' p' => fun xy => (fst xy, transfer_forall_parse_of _ _ _ _ p' (snd xy)) end.
imports: Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.Transfer