proposition: Lemma morph_id : morph OA OA (fun x => x).
proof: Proof. intros. constructor. apply L.morph_id. apply L. intros; eapply reflexivity. eapply reflexivity. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat