fact: Structure prespectful10 (clo: rel -> rel) : Prop := prespect10_intro { prespect10_mon: monotone10 clo; prespect10_respect : forall l r (LE: l <10= r) (GF: l <10= gf r), clo l <10= paco10 gf (r \10/ clo r); }.
imports: Program.Basics Paco(paco10 pacotac)