fact: Structure wrespectful5 (clo: rel -> rel) : Prop := wrespect5_intro { wrespect5_mon: monotone5 clo; wrespect5_respect : forall l r (LE: l <5= r) (GF: l <5= gf r), clo l <5= gf (rclo5 clo r); }.
imports: Program.Basics Paco(paco5 pacotac)