fact: Structure wrespectful13 (clo: rel -> rel) : Prop := wrespect13_intro { wrespect13_mon: monotone13 clo; wrespect13_respect : forall l r (LE: l <13= r) (GF: l <13= gf r), clo l <13= gf (rclo13 clo r); }.
imports: Program.Basics Paco(paco13 pacotac)