fact: Structure prespectful9 (clo: rel -> rel) : Prop := prespect9_intro { prespect9_mon: monotone9 clo; prespect9_respect : forall l r (LE: l <9= r) (GF: l <9= gf r), clo l <9= paco9 gf (r \9/ clo r); }.
imports: Program.Basics Paco(paco9 pacotac)