proposition: Lemma compRen'_pure_term (sigmapure_term : ( nat ) -> pure_term ) (zetapure_term : ( nat ) -> nat ) : funcomp (ren_pure_term zetapure_term) (subst_pure_term sigmapure_term) === subst_pure_term (funcomp (ren_pure_term zetapure_term) sigmapure_term) .
proof: Proof. exact ((fun n => compRen_pure_term sigmapure_term zetapure_term n)). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms