fact: Structure grespectful0 (clo: rel -> rel) : Prop := grespect0_intro { grespect0_mon: monotone0 clo; grespect0_respect : forall l r (LE: l <0= r) (GF: l <0= gf r), clo l <0= rclo0 (cpn0 gf) (gf (rclo0 (clo \1/ gupaco0 gf (cpn0 gf)) r)); }.
imports: Program.Basics Paco(paco0 pacotac)