fact: Structure prespectful4 (clo: rel -> rel) : Prop := prespect4_intro { prespect4_mon: monotone4 clo; prespect4_respect : forall l r (LE: l <4= r) (GF: l <4= gf r), clo l <4= paco4 gf (r \4/ clo r); }.
imports: Program.Basics Paco(paco4 pacotac)