proposition: Lemma renRen'_poly_type (xipoly_type : ( nat ) -> nat ) (zetapoly_type : ( nat ) -> nat ) : funcomp (ren_poly_type zetapoly_type) (ren_poly_type xipoly_type) === ren_poly_type (funcomp zetapoly_type xipoly_type) .
proof: Proof. exact ((fun n => renRen_poly_type xipoly_type zetapoly_type n)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms