fact: Structure wrespectful12 (clo: rel -> rel) : Prop := wrespect12_intro { wrespect12_mon: monotone12 clo; wrespect12_respect : forall l r (LE: l <12= r) (GF: l <12= gf r), clo l <12= gf (rclo12 clo r); }.
imports: Program.Basics Paco(paco12 pacotac)