proposition: Lemma args_for_related_related_map {T v1 v2} (f := @meaning _) : (args_for_related (T := T) (fun T (m : Term interp_TypeCode T) (n : Term (normalized_of interp_TypeCode) T) => related (interp_Term m) (f T n)) v1 v2) -> (args_for_related (fun T => Proper_relation_for T) (map_args_for (@interp_Term) v1) (map_args_for (@interp_Term) (unmeanings (meanings f v2)))).
proof: Proof. subst f; revert v2. induction v1; intro; pose proof (invert_args_for_ex v2) as H'; simpl in *; [ destruct H' as [? [? ?]] | subst; split; reflexivity ]; subst; simpl in *. intros [H0 H1]; split; try assumption; [ | apply IHv1; assumption ]; clear IHv1. apply reify_and_reflect_correct; assumption. 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