fact: Structure grespectful6 (clo: rel -> rel) : Prop := grespect6_intro { grespect6_mon: monotone6 clo; grespect6_respect : forall l r (LE: l <6= r) (GF: l <6= gf r), clo l <6= rclo6 (cpn6 gf) (gf (rclo6 (clo \7/ gupaco6 gf (cpn6 gf)) r)); }.
imports: Program.Basics Paco(paco6 pacotac)