proposition: Lemma asimpl_id_id_l X Y (f : X -> Y) : id >> f ≡ f.
proof: Proof. intros x; easy. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid