proposition: Lemma renComp'_pure_term (xipure_term : ( nat ) -> nat ) (taupure_term : ( nat ) -> pure_term ) : funcomp (subst_pure_term taupure_term) (ren_pure_term xipure_term) === subst_pure_term (funcomp taupure_term xipure_term) .
proof: Proof. exact ((fun n => renComp_pure_term xipure_term taupure_term n)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms