fact: Definition f : Hi nat R==> (Lo nat R=> Lo nat) := [< fun (hi : ⟬Hi nat⟭) => [< fun lo : ⟬Lo nat⟭ => lo | Lo nat >] | Lo nat R=> Lo nat >].
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase) Relational(Category RelativeMonads EnrichedSetting)