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