proposition: Lemma asimpl_scons_comp Z t s (f : term -> Z) : (t .: s) >> f ≡ ((f t) .: (s >> f)).
proof: Proof. intros [|n]; easy. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid