fact: Structure grespectful11 (clo: rel -> rel) : Prop := grespect11_intro { grespect11_mon: monotone11 clo; grespect11_respect : forall l r (LE: l <11= r) (GF: l <11= gf r), clo l <11= rclo11 (cpn11 gf) (gf (rclo11 (clo \12/ gupaco11 gf (cpn11 gf)) r)); }.
imports: Program.Basics Paco(paco11 pacotac)