proposition: Lemma renComp'_poly_type (xipoly_type : ( nat ) -> nat ) (taupoly_type : ( nat ) -> poly_type ) : funcomp (subst_poly_type taupoly_type) (ren_poly_type xipoly_type) === subst_poly_type (funcomp taupoly_type xipoly_type) .
proof: Proof. exact ((fun n => renComp_poly_type xipoly_type taupoly_type n)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms