fact: Structure prespectful3 (clo: rel -> rel) : Prop := prespect3_intro { prespect3_mon: monotone3 clo; prespect3_respect : forall l r (LE: l <3= r) (GF: l <3= gf r), clo l <3= paco3 gf (r \3/ clo r); }.
imports: Program.Basics Paco(paco3 pacotac)