proposition: Lemma asimpl_t_comp t s1 s2 : t`[s1]`[s2] = t`[s1 >> subst_term s2].
proof: Proof. apply subst_term_comp. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid