fact: Structure grespectful9 (clo: rel -> rel) : Prop := grespect9_intro { grespect9_mon: monotone9 clo; grespect9_respect : forall l r (LE: l <9= r) (GF: l <9= gf r), clo l <9= rclo9 (cpn9 gf) (gf (rclo9 (clo \10/ gupaco9 gf (cpn9 gf)) r)); }.
imports: Program.Basics Paco(paco9 pacotac)