proposition: Lemma Map_identity : forall X (a:StepF X), (fun x => x) ^@> a = a.
proof: Proof. exact Ap_identity. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields