fact: Structure grespectful3 (clo: rel -> rel) : Prop := grespect3_intro { grespect3_mon: monotone3 clo; grespect3_respect : forall l r (LE: l <3= r) (GF: l <3= gf r), clo l <3= rclo3 (cpn3 gf) (gf (rclo3 (clo \4/ gupaco3 gf (cpn3 gf)) r)); }.
imports: Program.Basics Paco(paco3 pacotac)