fact: Structure prespectful12 (clo: rel -> rel) : Prop := prespect12_intro { prespect12_mon: monotone12 clo; prespect12_respect : forall l r (LE: l <12= r) (GF: l <12= gf r), clo l <12= paco12 gf (r \12/ clo r); }.
imports: Program.Basics Paco(paco12 pacotac)