proposition: Lemma compRen_poly_type (sigmapoly_type : ( nat ) -> poly_type ) (zetapoly_type : ( nat ) -> nat ) (s : poly_type ) : ren_poly_type zetapoly_type (subst_poly_type sigmapoly_type s) = subst_poly_type (funcomp (ren_poly_type zetapoly_type) sigmapoly_type) s .
proof: Proof. exact (compSubstRen_poly_type sigmapoly_type zetapoly_type (_) (fun n => eq_refl) s). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms