fact: Structure grespectful2 (clo: rel -> rel) : Prop := grespect2_intro { grespect2_mon: monotone2 clo; grespect2_respect : forall l r (LE: l <2= r) (GF: l <2= gf r), clo l <2= rclo2 (cpn2 gf) (gf (rclo2 (clo \3/ gupaco2 gf (cpn2 gf)) r)); }.
imports: Program.Basics Paco(paco2 pacotac)