fact: Structure prespectful8 (clo: rel -> rel) : Prop := prespect8_intro { prespect8_mon: monotone8 clo; prespect8_respect : forall l r (LE: l <8= r) (GF: l <8= gf r), clo l <8= paco8 gf (r \8/ clo r); }.
imports: Program.Basics Paco(paco8 pacotac)