proposition: Lemma Term_equiv_syntactify_list_map {var1 var2 G A} {T : SimpleTypeCode} (f : A -> Term var1 T) (g : A -> Term var2 T) (ls : list A) (H : forall x, List.In x ls -> Term_equiv G (f x) (g x)) : Term_equiv G (Syntactify.syntactify_list (List.map f ls)) (Syntactify.syntactify_list (List.map g ls)).
proof: Proof. apply Term_equiv_syntactify_list. { rewrite !List.map_length; reflexivity. } { rewrite ListFacts.combine_map_l, ListFacts.combine_map_r, List.map_map; simpl. intros ?? H'. apply List.in_map_iff in H'. pose proof (@ListFacts.map_combine_id A _ (fun x => x) ls) as H''. rewrite List.map_id in H''. rewrite H'' in H'; clear H''. destruct H' as [[? ?] [H'0 H'1]]. apply List.in_map_iff in H'1. destruct H'1 as [? [H'1 H'2]]. inversion H'1; clear H'1; subst; simpl in *. inversion H'0; clear H'0; subst; simpl in *. eauto. } Qed.
imports: Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.BaseTypes Fiat.Parsers.BooleanRecognizerOptimizedReflective Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.SyntaxEquivalence Fiat.Parsers.Reflective.ParserSoundnessOptimized Fiat.Parsers.Reflective.ParserPartialUnfold Fiat.Parsers.Splitters.RDPList Fiat.Parsers.StringLike.Core