fact: Structure wrespectful9 (clo: rel -> rel) : Prop := wrespect9_intro { wrespect9_mon: monotone9 clo; wrespect9_respect : forall l r (LE: l <9= r) (GF: l <9= gf r), clo l <9= gf (rclo9 clo r); }.
imports: Program.Basics Paco(paco9 pacotac)