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