fact: Structure wrespectful1 (clo: rel -> rel) : Prop := wrespect1_intro { wrespect1_mon: monotone1 clo; wrespect1_respect : forall l r (LE: l <1= r) (GF: l <1= gf r), clo l <1= gf (rclo1 clo r); }.
imports: Program.Basics Paco(paco1 pacotac)