proposition: Lemma specific_meaning_correct t r val v1 v2 (Hrel : args_for_related (fun T' m n => @related T' (interp_Term m) (meaning n)) v1 v2) (Heq : specific_meaning r (meanings (@meaning interp_TypeCode) v2) = Some val) : interp_Term (@RLiteralApp _ t r v1) = interp_Term val.
proof: Proof. destruct r; simpl in Heq; unfold specific_meaning_apply1, specific_meaning_apply2 in *; try solve [ simpler_meaning; meaning_tac ]. { simpler_meaning; meaning_tac. apply interp_apply_meaning_helper; simpl; try assumption; []. apply list_rect_nodep_meaning_correct; simpl; eauto with nocore. simpler_meaning; meaning_tac. } { simpler_meaning; meaning_tac. rewrite Nat.add_comm; meaning_tac. } 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