fact: Structure grespectful5 (clo: rel -> rel) : Prop := grespect5_intro { grespect5_mon: monotone5 clo; grespect5_respect : forall l r (LE: l <5= r) (GF: l <5= gf r), clo l <5= rclo5 (cpn5 gf) (gf (rclo5 (clo \6/ gupaco5 gf (cpn5 gf)) r)); }.
imports: Program.Basics Paco(paco5 pacotac)