fact: Structure wrespectful2 (clo: rel -> rel) : Prop := wrespect2_intro { wrespect2_mon: monotone2 clo; wrespect2_respect : forall l r (LE: l <2= r) (GF: l <2= gf r), clo l <2= gf (rclo2 clo r); }.
imports: Program.Basics Paco(paco2 pacotac)