proposition: Lemma asimpl_t_id t : t`[var] = t.
proof: Proof. now apply subst_term_id. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid