proposition: Lemma renRen'_term (xipoly_type : ( nat ) -> nat ) (xiterm : ( nat ) -> nat ) (zetapoly_type : ( nat ) -> nat ) (zetaterm : ( nat ) -> nat ) : funcomp (ren_term zetapoly_type zetaterm) (ren_term xipoly_type xiterm) === ren_term (funcomp zetapoly_type xipoly_type) (funcomp zetaterm xiterm) .
proof: Proof. exact ((fun n => renRen_term xipoly_type xiterm zetapoly_type zetaterm n)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms