proposition: Lemma asimpl_f_ext t s1 s2 : s1 ≡ s2 -> t[s1] = t[s2].
proof: Proof. apply subst_ext. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid