proposition: Lemma meaning_correct : forall G t e1 e2, Term_equiv G e1 e2 -> (forall t' v1 v2, List.In (vars v1 v2) G -> @related t' v1 v2) -> @related t (interp_Term e1) (meaning e2).
proof: Proof. unfold interp_Term; induction 1 ; try solve [ simpler; eauto ]. { simpler. repeat match goal with | [ H : args_for_related_ind _ _ _ |- _ ] => apply args_for_related_noind_ind in H | [ H : args_for_related (fun x y z => ?P -> _) _ _ |- _ ] => setoid_rewrite <- args_for_related_impl in H | _ => progress simpl_interp_Term_in_all | [ H : ?A -> ?B, H' : ?A |- _ ] => specialize (H H') | [ f : RLiteralTerm _ |- _ ] => destruct f | [ |- apply_args_for _ _ = apply_args_for _ _ ] => apply apply_args_for_Proper; [ apply RLiteralTerm_Proper | apply args_for_related_related_map; assumption ] | [ |- context[specific_meaning ?r ?x] ] => destruct (specific_meaning r x) eqn:? end. eapply specific_meaning_correct; eassumption. } 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