proposition: Lemma interp_apply_meaning_helper T f f' (Hf : @related T f f') args args' (Hargs : args_for_related (fun T' m n => related (interp_Term m) (meaning n)) args args') : apply_args_for f (map_args_for (fun _ t => interp_Term t) args) = interp_Term (apply_meaning_helper (meanings (@meaning interp_TypeCode) args') f').
proof: Proof. apply args_for_related_noind_ind in Hargs. revert f f' Hf. induction Hargs; [ | solve [ simpl; trivial ] ]. apply args_for_related_noind_ind in Hargs. simpl in *. eauto with nocore. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Classes.Morphisms Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.PartialUnfold Fiat.Parsers.Reflective.SyntaxEquivalence Fiat.Parsers.Reflective.Morphisms Fiat.Common.List.ListFacts Fiat.Common.Equality