fact: Structure grespectful7 (clo: rel -> rel) : Prop := grespect7_intro { grespect7_mon: monotone7 clo; grespect7_respect : forall l r (LE: l <7= r) (GF: l <7= gf r), clo l <7= rclo7 (cpn7 gf) (gf (rclo7 (clo \8/ gupaco7 gf (cpn7 gf)) r)); }.
imports: Program.Basics Paco(paco7 pacotac)