proposition: Lemma asimpl_var_id_r (s : nat->term) : s >> subst_term var ≡ s.
proof: Proof. intros n. apply asimpl_t_id. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid