fact: Structure grespectful8 (clo: rel -> rel) : Prop := grespect8_intro { grespect8_mon: monotone8 clo; grespect8_respect : forall l r (LE: l <8= r) (GF: l <8= gf r), clo l <8= rclo8 (cpn8 gf) (gf (rclo8 (clo \9/ gupaco8 gf (cpn8 gf)) r)); }.
imports: Program.Basics Paco(paco8 pacotac)