fact: Structure grespectful14 (clo: rel -> rel) : Prop := grespect14_intro { grespect14_mon: monotone14 clo; grespect14_respect : forall l r (LE: l <14= r) (GF: l <14= gf r), clo l <14= rclo14 (cpn14 gf) (gf (rclo14 (clo \15/ gupaco14 gf (cpn14 gf)) r)); }.
imports: Program.Basics Paco(paco14 pacotac)