proposition: Lemma morph_compose {B OB} {tB : t B OB} {C OC} {tC : t C OC} (f : A -> B) (g : B -> C) : morph OA OB f -> morph OB OC g -> morph OA OC (fun x => g (f x)).
proof: Proof. intros. constructor. - eapply L.morph_compose; (apply L || (eapply f_L; eassumption)). - intros. rewrite <- (f_sup H0). rewrite (f_eq H0). reflexivity. rewrite (f_sup H). reflexivity. - rewrite <- (f_top H0). rewrite (f_eq H0). reflexivity. rewrite (f_top H). reflexivity. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat