fact: Structure grespectful13 (clo: rel -> rel) : Prop := grespect13_intro { grespect13_mon: monotone13 clo; grespect13_respect : forall l r (LE: l <13= r) (GF: l <13= gf r), clo l <13= rclo13 (cpn13 gf) (gf (rclo13 (clo \14/ gupaco13 gf (cpn13 gf)) r)); }.
imports: Program.Basics Paco(paco13 pacotac)