proposition: Lemma renRen'_pure_term (xipure_term : ( nat ) -> nat ) (zetapure_term : ( nat ) -> nat ) : funcomp (ren_pure_term zetapure_term) (ren_pure_term xipure_term) === ren_pure_term (funcomp zetapure_term xipure_term) .
proof: Proof. exact ((fun n => renRen_pure_term xipure_term zetapure_term n)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms