proposition: Lemma asimpl_var_id_l_ca X s (t:term -> X) : var >> (subst_term s >> t) ≡ s >> t.
proof: Proof. easy. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid