proposition: Lemma Term_equiv_syntactify_list {var1 var2 G} {T : SimpleTypeCode} (ls1 : list (Term var1 T)) (ls2 : list (Term var2 T)) (Hlen : List.length ls1 = List.length ls2) (H : forall x y, List.In (x, y) (List.combine ls1 ls2) -> Term_equiv G x y) : Term_equiv G (Syntactify.syntactify_list ls1) (Syntactify.syntactify_list ls2).
proof: Proof. revert dependent ls2; induction ls1 as [|x xs IHxs]; simpl; (destruct ls2; simpl; try congruence; []); intros Hlen H; match goal with | [ |- Term_equiv ?G (RLiteralApp ?f ?v1) (RLiteralApp ?f ?v2) ] => apply (@EqLiteralApp _ _ G _ f v1 v2) end; repeat constructor; 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