fact: Structure grespectful1 (clo: rel -> rel) : Prop := grespect1_intro { grespect1_mon: monotone1 clo; grespect1_respect : forall l r (LE: l <1= r) (GF: l <1= gf r), clo l <1= rclo1 (cpn1 gf) (gf (rclo1 (clo \2/ gupaco1 gf (cpn1 gf)) r)); }.
imports: Program.Basics Paco(paco1 pacotac)