proposition: Lemma compComp_pure_term (sigmapure_term : ( nat ) -> pure_term ) (taupure_term : ( nat ) -> pure_term ) (s : pure_term ) : subst_pure_term taupure_term (subst_pure_term sigmapure_term s) = subst_pure_term (funcomp (subst_pure_term taupure_term) sigmapure_term) s .
proof: Proof. exact (compSubstSubst_pure_term sigmapure_term taupure_term (_) (fun n => eq_refl) s). Qed.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms