proposition: Lemma asimpl_subst_merge (t r : nat -> term) : subst_term t >> subst_term r ≡ subst_term (t >> subst_term r).
proof: Proof. intros n; unfold funcomp. now rewrite subst_term_comp. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid