fact: Structure grespectful12 (clo: rel -> rel) : Prop := grespect12_intro { grespect12_mon: monotone12 clo; grespect12_respect : forall l r (LE: l <12= r) (GF: l <12= gf r), clo l <12= rclo12 (cpn12 gf) (gf (rclo12 (clo \13/ gupaco12 gf (cpn12 gf)) r)); }.
imports: Program.Basics Paco(paco12 pacotac)