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