fact: Structure prespectful7 (clo: rel -> rel) : Prop := prespect7_intro { prespect7_mon: monotone7 clo; prespect7_respect : forall l r (LE: l <7= r) (GF: l <7= gf r), clo l <7= paco7 gf (r \7/ clo r); }.
imports: Program.Basics Paco(paco7 pacotac)