fact: Definition pointwise_ops `(OB : forall a : A, Ops (B a)) : Ops (forall a, B a) := {| LOps := L.pointwise_ops (fun _ => LOps) ; sup := fun _ f => fun x => sup (fun i => f i x) |}.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat