proposition: Lemma list_rect_nodep_meaning_correct {A : SimpleTypeCode} {P} f f' n n' (Hn : @related P n n') (Hf : @related (A --> clist A --> P --> P) f f') (ls : list (Term interp_TypeCode A)) : related (Operations.List.list_rect_nodep n f (List.map (@interp_Term _) ls)) (Operations.List.list_rect_nodep n' (fun x xs => f' x (Syntactify.syntactify_list xs)) ls).
proof: Proof. induction ls; simpl in *; [ assumption | ]. apply Hf; eauto using eq_refl, @interp_Term_syntactify_list 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