fact: Structure prespectful13 (clo: rel -> rel) : Prop := prespect13_intro { prespect13_mon: monotone13 clo; prespect13_respect : forall l r (LE: l <13= r) (GF: l <13= gf r), clo l <13= paco13 gf (r \13/ clo r); }.
imports: Program.Basics Paco(paco13 pacotac)