fact: Structure prespectful5 (clo: rel -> rel) : Prop := prespect5_intro { prespect5_mon: monotone5 clo; prespect5_respect : forall l r (LE: l <5= r) (GF: l <5= gf r), clo l <5= paco5 gf (r \5/ clo r); }.
imports: Program.Basics Paco(paco5 pacotac)