proposition: Lemma renComp_term (xipoly_type : ( nat ) -> nat ) (xiterm : ( nat ) -> nat ) (taupoly_type : ( nat ) -> poly_type ) (tauterm : ( nat ) -> term ) (s : term ) : subst_term taupoly_type tauterm (ren_term xipoly_type xiterm s) = subst_term (funcomp taupoly_type xipoly_type) (funcomp tauterm xiterm) s .
proof: Proof. exact (compRenSubst_term xipoly_type xiterm taupoly_type tauterm (_) (_) (fun n => eq_refl) (fun n => eq_refl) s). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms