fact: Structure wrespectful0 (clo: rel -> rel) : Prop := wrespect0_intro { wrespect0_mon: monotone0 clo; wrespect0_respect : forall l r (LE: l <0= r) (GF: l <0= gf r), clo l <0= gf (rclo0 clo r); }.
imports: Program.Basics Paco(paco0 pacotac)