proposition: Lemma renRen_pure_term (xipure_term : ( nat ) -> nat ) (zetapure_term : ( nat ) -> nat ) (s : pure_term ) : ren_pure_term zetapure_term (ren_pure_term xipure_term s) = ren_pure_term (funcomp zetapure_term xipure_term) s .
proof: Proof. exact (compRenRen_pure_term xipure_term zetapure_term (_) (fun n => eq_refl) s). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms