proposition: Lemma compComp'_term (sigmapoly_type : ( nat ) -> poly_type ) (sigmaterm : ( nat ) -> term ) (taupoly_type : ( nat ) -> poly_type ) (tauterm : ( nat ) -> term ) : funcomp (subst_term taupoly_type tauterm) (subst_term sigmapoly_type sigmaterm) === subst_term (funcomp (subst_poly_type taupoly_type) sigmapoly_type) (funcomp (subst_term taupoly_type tauterm) sigmaterm) .
proof: Proof. exact ((fun n => compComp_term sigmapoly_type sigmaterm taupoly_type tauterm n)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms