proposition: Lemma compRen'_term (sigmapoly_type : ( nat ) -> poly_type ) (sigmaterm : ( nat ) -> term ) (zetapoly_type : ( nat ) -> nat ) (zetaterm : ( nat ) -> nat ) : funcomp (ren_term zetapoly_type zetaterm) (subst_term sigmapoly_type sigmaterm) === subst_term (funcomp (ren_poly_type zetapoly_type) sigmapoly_type) (funcomp (ren_term zetapoly_type zetaterm) sigmaterm) .
proof: Proof. exact ((fun n => compRen_term sigmapoly_type sigmaterm zetapoly_type zetaterm n)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms