diff --git a/metasrc/gpaco.py b/metasrc/gpaco.py
index 6a3f796..a3a9e03 100644
--- a/metasrc/gpaco.py
+++ b/metasrc/gpaco.py
@@ -670,6 +670,17 @@
 print ("    }.")
 print ("Hint Constructors wrespectful"+str(n)+".")
 print ("")
+print ("Structure prespectful"+str(n)+" (clo: rel -> rel) : Prop :=")
+print ("  prespect"+str(n)+"_intro {")
+print ("      prespect"+str(n)+"_mon: monotone"+str(n)+" clo;")
+print ("      prespect"+str(n)+"_respect :")
+print ("        forall l r")
+print ("               (LE: l <"+str(n)+"= r)")
+print ("               (GF: l <"+str(n)+"= gf r),")
+print ("        clo l <"+str(n)+"= paco"+str(n)+" gf (r \\"+str(n)+"/ clo r);")
+print ("    }.")
+print ("Hint Constructors prespectful"+str(n)+".")
+print ("")
 print ("Definition gf'"+str(n)+" := id /"+str(n+1)+"\\ gf.")
 print ("")
 print ("Definition compatible'"+str(n)+" := compatible"+str(n)+" gf'"+str(n)+".")
@@ -690,6 +701,36 @@
 print ("    + intros. apply rclo"+str(n)+"_rclo, PR.")
 print ("Qed.")
 print ("")
+print ("Lemma prespect"+str(n)+"_compatible'")
+print ("      clo (RES: prespectful"+str(n)+" clo):")
+print ("  compatible'"+str(n)+" (fun r => upaco"+str(n)+" gf (r \\"+str(n)+"/ clo r)).")
+print ("Proof.")
+print ("  econstructor.")
+print ("  { red; intros. eapply upaco"+str(n)+"_mon. apply IN.")
+print ("    intros. destruct PR.")
+print ("    - left. apply LE, H.")
+print ("    - right. eapply RES. apply H. intros. apply LE, PR. }")
+print ("")
+print ("  intros r.")
+print ("  assert (LEM: (gf'"+str(n)+" r \\"+str(n)+"/ clo (gf'"+str(n)+" r)) <"+str(n)+"= (r \\"+str(n)+"/ clo r)).")
+print ("  { intros. destruct PR.")
+print ("    - left. apply H.")
+print ("    - right. eapply RES. apply H. intros. apply PR.")
+print ("  }")
+print ("")
+print ("  intros. destruct PR.")
+print ("  - split.")
+print ("    + left. eapply paco"+str(n)+"_mon. apply H. apply LEM.")
+print ("    + apply paco"+str(n)+"_unfold; [apply gf_mon|].")
+print ("      eapply paco"+str(n)+"_mon. apply H. apply LEM.")
+print ("  - split.")
+print ("    + right. apply LEM. apply H.")
+print ("    + destruct H.")
+print ("      * eapply gf_mon. apply H. intros. right. left. apply PR.")
+print ("      * apply paco"+str(n)+"_unfold; [apply gf_mon|].")
+print ("        eapply RES, H; intros; apply PR.")
+print ("Qed.")
+print ("")
 print ("Lemma compat"+str(n)+"_compatible'")
 print ("      clo (COM: compatible"+str(n)+" gf clo):")
 print ("  compatible'"+str(n)+" clo.")
@@ -740,6 +781,14 @@
 print ("  eapply rclo"+str(n)+"_clo_base, PR.")
 print ("Qed.")
 print ("")
+print ("Lemma prespect"+str(n)+"_companion")
+print ("      clo (RES: prespectful"+str(n)+" clo):")
+print ("  clo <"+str(n+1)+"= cpn"+str(n)+" gf.")
+print ("Proof.")
+print ("  intros. eapply compatible'"+str(n)+"_companion. apply prespect"+str(n)+"_compatible'. apply RES.")
+print ("  right. right. apply PR.")
+print ("Qed.")
+print ("")
 print ("Lemma wrespect"+str(n)+"_uclo")
 print ("      clo (RES: wrespectful"+str(n)+" clo):")
 print ("  clo <"+str(n+1)+"= gupaco"+str(n)+" gf (cpn"+str(n)+" gf).")
@@ -747,6 +796,13 @@
 print ("  intros. eapply gpaco"+str(n)+"_clo, wrespect"+str(n)+"_companion, PR. apply RES.")
 print ("Qed.")
 print ("")
+print ("Lemma prespect"+str(n)+"_uclo")
+print ("      clo (RES: prespectful"+str(n)+" clo):")
+print ("  clo <"+str(n+1)+"= gupaco"+str(n)+" gf (cpn"+str(n)+" gf).")
+print ("Proof.")
+print ("  intros. eapply gpaco"+str(n)+"_clo, prespect"+str(n)+"_companion, PR. apply RES.")
+print ("Qed.")
+print ("")
 print ("End Respectful.")
 print ("")
 print ("End GeneralizedPaco"+str(n)+".")
@@ -759,3 +815,4 @@
 print ("Hint Resolve rclo"+str(n)+"_base : paco.")
 print ("Hint Constructors gpaco"+str(n)+" : paco.")
 print ("Hint Resolve wrespect"+str(n)+"_uclo : paco.")
+print ("Hint Resolve prespect"+str(n)+"_uclo : paco.")
diff --git a/src/gpaco0.v b/src/gpaco0.v
index 229e815..9b377df 100644
--- a/src/gpaco0.v
+++ b/src/gpaco0.v
@@ -657,6 +657,17 @@ Structure wrespectful0 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful0.
 
+Structure prespectful0 (clo: rel -> rel) : Prop :=
+  prespect0_intro {
+      prespect0_mon: monotone0 clo;
+      prespect0_respect :
+        forall l r
+               (LE: l <0= r)
+               (GF: l <0= gf r),
+        clo l <0= paco0 gf (r \0/ clo r);
+    }.
+Hint Constructors prespectful0.
+
 Definition gf'0 := id /1\ gf.
 
 Definition compatible'0 := compatible0 gf'0.
@@ -677,6 +688,36 @@ Proof.
     + intros. apply rclo0_rclo, PR.
 Qed.
 
+Lemma prespect0_compatible'
+      clo (RES: prespectful0 clo):
+  compatible'0 (fun r => upaco0 gf (r \0/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco0_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'0 r \0/ clo (gf'0 r)) <0= (r \0/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco0_mon. apply H. apply LEM.
+    + apply paco0_unfold; [apply gf_mon|].
+      eapply paco0_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco0_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat0_compatible'
       clo (COM: compatible0 gf clo):
   compatible'0 clo.
@@ -727,6 +768,14 @@ Proof.
   eapply rclo0_clo_base, PR.
 Qed.
 
+Lemma prespect0_companion
+      clo (RES: prespectful0 clo):
+  clo <1= cpn0 gf.
+Proof.
+  intros. eapply compatible'0_companion. apply prespect0_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect0_uclo
       clo (RES: wrespectful0 clo):
   clo <1= gupaco0 gf (cpn0 gf).
@@ -734,6 +783,13 @@ Proof.
   intros. eapply gpaco0_clo, wrespect0_companion, PR. apply RES.
 Qed.
 
+Lemma prespect0_uclo
+      clo (RES: prespectful0 clo):
+  clo <1= gupaco0 gf (cpn0 gf).
+Proof.
+  intros. eapply gpaco0_clo, prespect0_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco0.
@@ -746,3 +802,4 @@ Hint Resolve gpaco0_final : paco.
 Hint Resolve rclo0_base : paco.
 Hint Constructors gpaco0 : paco.
 Hint Resolve wrespect0_uclo : paco.
+Hint Resolve prespect0_uclo : paco.
diff --git a/src/gpaco1.v b/src/gpaco1.v
index a0192e8..84098c6 100644
--- a/src/gpaco1.v
+++ b/src/gpaco1.v
@@ -658,6 +658,17 @@ Structure wrespectful1 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful1.
 
+Structure prespectful1 (clo: rel -> rel) : Prop :=
+  prespect1_intro {
+      prespect1_mon: monotone1 clo;
+      prespect1_respect :
+        forall l r
+               (LE: l <1= r)
+               (GF: l <1= gf r),
+        clo l <1= paco1 gf (r \1/ clo r);
+    }.
+Hint Constructors prespectful1.
+
 Definition gf'1 := id /2\ gf.
 
 Definition compatible'1 := compatible1 gf'1.
@@ -678,6 +689,36 @@ Proof.
     + intros. apply rclo1_rclo, PR.
 Qed.
 
+Lemma prespect1_compatible'
+      clo (RES: prespectful1 clo):
+  compatible'1 (fun r => upaco1 gf (r \1/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco1_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'1 r \1/ clo (gf'1 r)) <1= (r \1/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco1_mon. apply H. apply LEM.
+    + apply paco1_unfold; [apply gf_mon|].
+      eapply paco1_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco1_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat1_compatible'
       clo (COM: compatible1 gf clo):
   compatible'1 clo.
@@ -728,6 +769,14 @@ Proof.
   eapply rclo1_clo_base, PR.
 Qed.
 
+Lemma prespect1_companion
+      clo (RES: prespectful1 clo):
+  clo <2= cpn1 gf.
+Proof.
+  intros. eapply compatible'1_companion. apply prespect1_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect1_uclo
       clo (RES: wrespectful1 clo):
   clo <2= gupaco1 gf (cpn1 gf).
@@ -735,6 +784,13 @@ Proof.
   intros. eapply gpaco1_clo, wrespect1_companion, PR. apply RES.
 Qed.
 
+Lemma prespect1_uclo
+      clo (RES: prespectful1 clo):
+  clo <2= gupaco1 gf (cpn1 gf).
+Proof.
+  intros. eapply gpaco1_clo, prespect1_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco1.
@@ -747,3 +803,4 @@ Hint Resolve gpaco1_final : paco.
 Hint Resolve rclo1_base : paco.
 Hint Constructors gpaco1 : paco.
 Hint Resolve wrespect1_uclo : paco.
+Hint Resolve prespect1_uclo : paco.
diff --git a/src/gpaco10.v b/src/gpaco10.v
index 2b1d522..76d2353 100644
--- a/src/gpaco10.v
+++ b/src/gpaco10.v
@@ -667,6 +667,17 @@ Structure wrespectful10 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful10.
 
+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);
+    }.
+Hint Constructors prespectful10.
+
 Definition gf'10 := id /11\ gf.
 
 Definition compatible'10 := compatible10 gf'10.
@@ -687,6 +698,36 @@ Proof.
     + intros. apply rclo10_rclo, PR.
 Qed.
 
+Lemma prespect10_compatible'
+      clo (RES: prespectful10 clo):
+  compatible'10 (fun r => upaco10 gf (r \10/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco10_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'10 r \10/ clo (gf'10 r)) <10= (r \10/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco10_mon. apply H. apply LEM.
+    + apply paco10_unfold; [apply gf_mon|].
+      eapply paco10_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco10_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat10_compatible'
       clo (COM: compatible10 gf clo):
   compatible'10 clo.
@@ -737,6 +778,14 @@ Proof.
   eapply rclo10_clo_base, PR.
 Qed.
 
+Lemma prespect10_companion
+      clo (RES: prespectful10 clo):
+  clo <11= cpn10 gf.
+Proof.
+  intros. eapply compatible'10_companion. apply prespect10_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect10_uclo
       clo (RES: wrespectful10 clo):
   clo <11= gupaco10 gf (cpn10 gf).
@@ -744,6 +793,13 @@ Proof.
   intros. eapply gpaco10_clo, wrespect10_companion, PR. apply RES.
 Qed.
 
+Lemma prespect10_uclo
+      clo (RES: prespectful10 clo):
+  clo <11= gupaco10 gf (cpn10 gf).
+Proof.
+  intros. eapply gpaco10_clo, prespect10_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco10.
@@ -756,3 +812,4 @@ Hint Resolve gpaco10_final : paco.
 Hint Resolve rclo10_base : paco.
 Hint Constructors gpaco10 : paco.
 Hint Resolve wrespect10_uclo : paco.
+Hint Resolve prespect10_uclo : paco.
diff --git a/src/gpaco11.v b/src/gpaco11.v
index df91152..e305976 100644
--- a/src/gpaco11.v
+++ b/src/gpaco11.v
@@ -668,6 +668,17 @@ Structure wrespectful11 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful11.
 
+Structure prespectful11 (clo: rel -> rel) : Prop :=
+  prespect11_intro {
+      prespect11_mon: monotone11 clo;
+      prespect11_respect :
+        forall l r
+               (LE: l <11= r)
+               (GF: l <11= gf r),
+        clo l <11= paco11 gf (r \11/ clo r);
+    }.
+Hint Constructors prespectful11.
+
 Definition gf'11 := id /12\ gf.
 
 Definition compatible'11 := compatible11 gf'11.
@@ -688,6 +699,36 @@ Proof.
     + intros. apply rclo11_rclo, PR.
 Qed.
 
+Lemma prespect11_compatible'
+      clo (RES: prespectful11 clo):
+  compatible'11 (fun r => upaco11 gf (r \11/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco11_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'11 r \11/ clo (gf'11 r)) <11= (r \11/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco11_mon. apply H. apply LEM.
+    + apply paco11_unfold; [apply gf_mon|].
+      eapply paco11_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco11_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat11_compatible'
       clo (COM: compatible11 gf clo):
   compatible'11 clo.
@@ -738,6 +779,14 @@ Proof.
   eapply rclo11_clo_base, PR.
 Qed.
 
+Lemma prespect11_companion
+      clo (RES: prespectful11 clo):
+  clo <12= cpn11 gf.
+Proof.
+  intros. eapply compatible'11_companion. apply prespect11_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect11_uclo
       clo (RES: wrespectful11 clo):
   clo <12= gupaco11 gf (cpn11 gf).
@@ -745,6 +794,13 @@ Proof.
   intros. eapply gpaco11_clo, wrespect11_companion, PR. apply RES.
 Qed.
 
+Lemma prespect11_uclo
+      clo (RES: prespectful11 clo):
+  clo <12= gupaco11 gf (cpn11 gf).
+Proof.
+  intros. eapply gpaco11_clo, prespect11_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco11.
@@ -757,3 +813,4 @@ Hint Resolve gpaco11_final : paco.
 Hint Resolve rclo11_base : paco.
 Hint Constructors gpaco11 : paco.
 Hint Resolve wrespect11_uclo : paco.
+Hint Resolve prespect11_uclo : paco.
diff --git a/src/gpaco12.v b/src/gpaco12.v
index e07bb7b..7e0fe28 100644
--- a/src/gpaco12.v
+++ b/src/gpaco12.v
@@ -669,6 +669,17 @@ Structure wrespectful12 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful12.
 
+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);
+    }.
+Hint Constructors prespectful12.
+
 Definition gf'12 := id /13\ gf.
 
 Definition compatible'12 := compatible12 gf'12.
@@ -689,6 +700,36 @@ Proof.
     + intros. apply rclo12_rclo, PR.
 Qed.
 
+Lemma prespect12_compatible'
+      clo (RES: prespectful12 clo):
+  compatible'12 (fun r => upaco12 gf (r \12/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco12_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'12 r \12/ clo (gf'12 r)) <12= (r \12/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco12_mon. apply H. apply LEM.
+    + apply paco12_unfold; [apply gf_mon|].
+      eapply paco12_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco12_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat12_compatible'
       clo (COM: compatible12 gf clo):
   compatible'12 clo.
@@ -739,6 +780,14 @@ Proof.
   eapply rclo12_clo_base, PR.
 Qed.
 
+Lemma prespect12_companion
+      clo (RES: prespectful12 clo):
+  clo <13= cpn12 gf.
+Proof.
+  intros. eapply compatible'12_companion. apply prespect12_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect12_uclo
       clo (RES: wrespectful12 clo):
   clo <13= gupaco12 gf (cpn12 gf).
@@ -746,6 +795,13 @@ Proof.
   intros. eapply gpaco12_clo, wrespect12_companion, PR. apply RES.
 Qed.
 
+Lemma prespect12_uclo
+      clo (RES: prespectful12 clo):
+  clo <13= gupaco12 gf (cpn12 gf).
+Proof.
+  intros. eapply gpaco12_clo, prespect12_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco12.
@@ -758,3 +814,4 @@ Hint Resolve gpaco12_final : paco.
 Hint Resolve rclo12_base : paco.
 Hint Constructors gpaco12 : paco.
 Hint Resolve wrespect12_uclo : paco.
+Hint Resolve prespect12_uclo : paco.
diff --git a/src/gpaco13.v b/src/gpaco13.v
index 3de8f49..04777dd 100644
--- a/src/gpaco13.v
+++ b/src/gpaco13.v
@@ -670,6 +670,17 @@ Structure wrespectful13 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful13.
 
+Structure prespectful13 (clo: rel -> rel) : Prop :=
+  prespect13_intro {
+      prespect13_mon: monotone13 clo;
+      prespect13_respect :
+        forall l r
+               (LE: l <13= r)
+               (GF: l <13= gf r),
+        clo l <13= paco13 gf (r \13/ clo r);
+    }.
+Hint Constructors prespectful13.
+
 Definition gf'13 := id /14\ gf.
 
 Definition compatible'13 := compatible13 gf'13.
@@ -690,6 +701,36 @@ Proof.
     + intros. apply rclo13_rclo, PR.
 Qed.
 
+Lemma prespect13_compatible'
+      clo (RES: prespectful13 clo):
+  compatible'13 (fun r => upaco13 gf (r \13/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco13_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'13 r \13/ clo (gf'13 r)) <13= (r \13/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco13_mon. apply H. apply LEM.
+    + apply paco13_unfold; [apply gf_mon|].
+      eapply paco13_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco13_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat13_compatible'
       clo (COM: compatible13 gf clo):
   compatible'13 clo.
@@ -740,6 +781,14 @@ Proof.
   eapply rclo13_clo_base, PR.
 Qed.
 
+Lemma prespect13_companion
+      clo (RES: prespectful13 clo):
+  clo <14= cpn13 gf.
+Proof.
+  intros. eapply compatible'13_companion. apply prespect13_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect13_uclo
       clo (RES: wrespectful13 clo):
   clo <14= gupaco13 gf (cpn13 gf).
@@ -747,6 +796,13 @@ Proof.
   intros. eapply gpaco13_clo, wrespect13_companion, PR. apply RES.
 Qed.
 
+Lemma prespect13_uclo
+      clo (RES: prespectful13 clo):
+  clo <14= gupaco13 gf (cpn13 gf).
+Proof.
+  intros. eapply gpaco13_clo, prespect13_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco13.
@@ -759,3 +815,4 @@ Hint Resolve gpaco13_final : paco.
 Hint Resolve rclo13_base : paco.
 Hint Constructors gpaco13 : paco.
 Hint Resolve wrespect13_uclo : paco.
+Hint Resolve prespect13_uclo : paco.
diff --git a/src/gpaco14.v b/src/gpaco14.v
index 4363fd6..c11b906 100644
--- a/src/gpaco14.v
+++ b/src/gpaco14.v
@@ -671,6 +671,17 @@ Structure wrespectful14 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful14.
 
+Structure prespectful14 (clo: rel -> rel) : Prop :=
+  prespect14_intro {
+      prespect14_mon: monotone14 clo;
+      prespect14_respect :
+        forall l r
+               (LE: l <14= r)
+               (GF: l <14= gf r),
+        clo l <14= paco14 gf (r \14/ clo r);
+    }.
+Hint Constructors prespectful14.
+
 Definition gf'14 := id /15\ gf.
 
 Definition compatible'14 := compatible14 gf'14.
@@ -691,6 +702,36 @@ Proof.
     + intros. apply rclo14_rclo, PR.
 Qed.
 
+Lemma prespect14_compatible'
+      clo (RES: prespectful14 clo):
+  compatible'14 (fun r => upaco14 gf (r \14/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco14_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'14 r \14/ clo (gf'14 r)) <14= (r \14/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco14_mon. apply H. apply LEM.
+    + apply paco14_unfold; [apply gf_mon|].
+      eapply paco14_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco14_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat14_compatible'
       clo (COM: compatible14 gf clo):
   compatible'14 clo.
@@ -741,6 +782,14 @@ Proof.
   eapply rclo14_clo_base, PR.
 Qed.
 
+Lemma prespect14_companion
+      clo (RES: prespectful14 clo):
+  clo <15= cpn14 gf.
+Proof.
+  intros. eapply compatible'14_companion. apply prespect14_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect14_uclo
       clo (RES: wrespectful14 clo):
   clo <15= gupaco14 gf (cpn14 gf).
@@ -748,6 +797,13 @@ Proof.
   intros. eapply gpaco14_clo, wrespect14_companion, PR. apply RES.
 Qed.
 
+Lemma prespect14_uclo
+      clo (RES: prespectful14 clo):
+  clo <15= gupaco14 gf (cpn14 gf).
+Proof.
+  intros. eapply gpaco14_clo, prespect14_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco14.
@@ -760,3 +816,4 @@ Hint Resolve gpaco14_final : paco.
 Hint Resolve rclo14_base : paco.
 Hint Constructors gpaco14 : paco.
 Hint Resolve wrespect14_uclo : paco.
+Hint Resolve prespect14_uclo : paco.
diff --git a/src/gpaco2.v b/src/gpaco2.v
index dedbbb1..26365a5 100644
--- a/src/gpaco2.v
+++ b/src/gpaco2.v
@@ -659,6 +659,17 @@ Structure wrespectful2 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful2.
 
+Structure prespectful2 (clo: rel -> rel) : Prop :=
+  prespect2_intro {
+      prespect2_mon: monotone2 clo;
+      prespect2_respect :
+        forall l r
+               (LE: l <2= r)
+               (GF: l <2= gf r),
+        clo l <2= paco2 gf (r \2/ clo r);
+    }.
+Hint Constructors prespectful2.
+
 Definition gf'2 := id /3\ gf.
 
 Definition compatible'2 := compatible2 gf'2.
@@ -679,6 +690,36 @@ Proof.
     + intros. apply rclo2_rclo, PR.
 Qed.
 
+Lemma prespect2_compatible'
+      clo (RES: prespectful2 clo):
+  compatible'2 (fun r => upaco2 gf (r \2/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco2_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'2 r \2/ clo (gf'2 r)) <2= (r \2/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco2_mon. apply H. apply LEM.
+    + apply paco2_unfold; [apply gf_mon|].
+      eapply paco2_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco2_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat2_compatible'
       clo (COM: compatible2 gf clo):
   compatible'2 clo.
@@ -729,6 +770,14 @@ Proof.
   eapply rclo2_clo_base, PR.
 Qed.
 
+Lemma prespect2_companion
+      clo (RES: prespectful2 clo):
+  clo <3= cpn2 gf.
+Proof.
+  intros. eapply compatible'2_companion. apply prespect2_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect2_uclo
       clo (RES: wrespectful2 clo):
   clo <3= gupaco2 gf (cpn2 gf).
@@ -736,6 +785,13 @@ Proof.
   intros. eapply gpaco2_clo, wrespect2_companion, PR. apply RES.
 Qed.
 
+Lemma prespect2_uclo
+      clo (RES: prespectful2 clo):
+  clo <3= gupaco2 gf (cpn2 gf).
+Proof.
+  intros. eapply gpaco2_clo, prespect2_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco2.
@@ -748,3 +804,4 @@ Hint Resolve gpaco2_final : paco.
 Hint Resolve rclo2_base : paco.
 Hint Constructors gpaco2 : paco.
 Hint Resolve wrespect2_uclo : paco.
+Hint Resolve prespect2_uclo : paco.
diff --git a/src/gpaco3.v b/src/gpaco3.v
index 974eb08..3eed727 100644
--- a/src/gpaco3.v
+++ b/src/gpaco3.v
@@ -660,6 +660,17 @@ Structure wrespectful3 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful3.
 
+Structure prespectful3 (clo: rel -> rel) : Prop :=
+  prespect3_intro {
+      prespect3_mon: monotone3 clo;
+      prespect3_respect :
+        forall l r
+               (LE: l <3= r)
+               (GF: l <3= gf r),
+        clo l <3= paco3 gf (r \3/ clo r);
+    }.
+Hint Constructors prespectful3.
+
 Definition gf'3 := id /4\ gf.
 
 Definition compatible'3 := compatible3 gf'3.
@@ -680,6 +691,36 @@ Proof.
     + intros. apply rclo3_rclo, PR.
 Qed.
 
+Lemma prespect3_compatible'
+      clo (RES: prespectful3 clo):
+  compatible'3 (fun r => upaco3 gf (r \3/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco3_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'3 r \3/ clo (gf'3 r)) <3= (r \3/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco3_mon. apply H. apply LEM.
+    + apply paco3_unfold; [apply gf_mon|].
+      eapply paco3_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco3_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat3_compatible'
       clo (COM: compatible3 gf clo):
   compatible'3 clo.
@@ -730,6 +771,14 @@ Proof.
   eapply rclo3_clo_base, PR.
 Qed.
 
+Lemma prespect3_companion
+      clo (RES: prespectful3 clo):
+  clo <4= cpn3 gf.
+Proof.
+  intros. eapply compatible'3_companion. apply prespect3_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect3_uclo
       clo (RES: wrespectful3 clo):
   clo <4= gupaco3 gf (cpn3 gf).
@@ -737,6 +786,13 @@ Proof.
   intros. eapply gpaco3_clo, wrespect3_companion, PR. apply RES.
 Qed.
 
+Lemma prespect3_uclo
+      clo (RES: prespectful3 clo):
+  clo <4= gupaco3 gf (cpn3 gf).
+Proof.
+  intros. eapply gpaco3_clo, prespect3_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco3.
@@ -749,3 +805,4 @@ Hint Resolve gpaco3_final : paco.
 Hint Resolve rclo3_base : paco.
 Hint Constructors gpaco3 : paco.
 Hint Resolve wrespect3_uclo : paco.
+Hint Resolve prespect3_uclo : paco.
diff --git a/src/gpaco4.v b/src/gpaco4.v
index 3f0bd6f..c2a3b4e 100644
--- a/src/gpaco4.v
+++ b/src/gpaco4.v
@@ -661,6 +661,17 @@ Structure wrespectful4 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful4.
 
+Structure prespectful4 (clo: rel -> rel) : Prop :=
+  prespect4_intro {
+      prespect4_mon: monotone4 clo;
+      prespect4_respect :
+        forall l r
+               (LE: l <4= r)
+               (GF: l <4= gf r),
+        clo l <4= paco4 gf (r \4/ clo r);
+    }.
+Hint Constructors prespectful4.
+
 Definition gf'4 := id /5\ gf.
 
 Definition compatible'4 := compatible4 gf'4.
@@ -681,6 +692,36 @@ Proof.
     + intros. apply rclo4_rclo, PR.
 Qed.
 
+Lemma prespect4_compatible'
+      clo (RES: prespectful4 clo):
+  compatible'4 (fun r => upaco4 gf (r \4/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco4_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'4 r \4/ clo (gf'4 r)) <4= (r \4/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco4_mon. apply H. apply LEM.
+    + apply paco4_unfold; [apply gf_mon|].
+      eapply paco4_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco4_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat4_compatible'
       clo (COM: compatible4 gf clo):
   compatible'4 clo.
@@ -731,6 +772,14 @@ Proof.
   eapply rclo4_clo_base, PR.
 Qed.
 
+Lemma prespect4_companion
+      clo (RES: prespectful4 clo):
+  clo <5= cpn4 gf.
+Proof.
+  intros. eapply compatible'4_companion. apply prespect4_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect4_uclo
       clo (RES: wrespectful4 clo):
   clo <5= gupaco4 gf (cpn4 gf).
@@ -738,6 +787,13 @@ Proof.
   intros. eapply gpaco4_clo, wrespect4_companion, PR. apply RES.
 Qed.
 
+Lemma prespect4_uclo
+      clo (RES: prespectful4 clo):
+  clo <5= gupaco4 gf (cpn4 gf).
+Proof.
+  intros. eapply gpaco4_clo, prespect4_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco4.
@@ -750,3 +806,4 @@ Hint Resolve gpaco4_final : paco.
 Hint Resolve rclo4_base : paco.
 Hint Constructors gpaco4 : paco.
 Hint Resolve wrespect4_uclo : paco.
+Hint Resolve prespect4_uclo : paco.
diff --git a/src/gpaco5.v b/src/gpaco5.v
index ac83bc2..b8b101c 100644
--- a/src/gpaco5.v
+++ b/src/gpaco5.v
@@ -662,6 +662,17 @@ Structure wrespectful5 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful5.
 
+Structure prespectful5 (clo: rel -> rel) : Prop :=
+  prespect5_intro {
+      prespect5_mon: monotone5 clo;
+      prespect5_respect :
+        forall l r
+               (LE: l <5= r)
+               (GF: l <5= gf r),
+        clo l <5= paco5 gf (r \5/ clo r);
+    }.
+Hint Constructors prespectful5.
+
 Definition gf'5 := id /6\ gf.
 
 Definition compatible'5 := compatible5 gf'5.
@@ -682,6 +693,36 @@ Proof.
     + intros. apply rclo5_rclo, PR.
 Qed.
 
+Lemma prespect5_compatible'
+      clo (RES: prespectful5 clo):
+  compatible'5 (fun r => upaco5 gf (r \5/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco5_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'5 r \5/ clo (gf'5 r)) <5= (r \5/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco5_mon. apply H. apply LEM.
+    + apply paco5_unfold; [apply gf_mon|].
+      eapply paco5_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco5_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat5_compatible'
       clo (COM: compatible5 gf clo):
   compatible'5 clo.
@@ -732,6 +773,14 @@ Proof.
   eapply rclo5_clo_base, PR.
 Qed.
 
+Lemma prespect5_companion
+      clo (RES: prespectful5 clo):
+  clo <6= cpn5 gf.
+Proof.
+  intros. eapply compatible'5_companion. apply prespect5_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect5_uclo
       clo (RES: wrespectful5 clo):
   clo <6= gupaco5 gf (cpn5 gf).
@@ -739,6 +788,13 @@ Proof.
   intros. eapply gpaco5_clo, wrespect5_companion, PR. apply RES.
 Qed.
 
+Lemma prespect5_uclo
+      clo (RES: prespectful5 clo):
+  clo <6= gupaco5 gf (cpn5 gf).
+Proof.
+  intros. eapply gpaco5_clo, prespect5_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco5.
@@ -751,3 +807,4 @@ Hint Resolve gpaco5_final : paco.
 Hint Resolve rclo5_base : paco.
 Hint Constructors gpaco5 : paco.
 Hint Resolve wrespect5_uclo : paco.
+Hint Resolve prespect5_uclo : paco.
diff --git a/src/gpaco6.v b/src/gpaco6.v
index f188008..60e539b 100644
--- a/src/gpaco6.v
+++ b/src/gpaco6.v
@@ -663,6 +663,17 @@ Structure wrespectful6 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful6.
 
+Structure prespectful6 (clo: rel -> rel) : Prop :=
+  prespect6_intro {
+      prespect6_mon: monotone6 clo;
+      prespect6_respect :
+        forall l r
+               (LE: l <6= r)
+               (GF: l <6= gf r),
+        clo l <6= paco6 gf (r \6/ clo r);
+    }.
+Hint Constructors prespectful6.
+
 Definition gf'6 := id /7\ gf.
 
 Definition compatible'6 := compatible6 gf'6.
@@ -683,6 +694,36 @@ Proof.
     + intros. apply rclo6_rclo, PR.
 Qed.
 
+Lemma prespect6_compatible'
+      clo (RES: prespectful6 clo):
+  compatible'6 (fun r => upaco6 gf (r \6/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco6_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'6 r \6/ clo (gf'6 r)) <6= (r \6/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco6_mon. apply H. apply LEM.
+    + apply paco6_unfold; [apply gf_mon|].
+      eapply paco6_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco6_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat6_compatible'
       clo (COM: compatible6 gf clo):
   compatible'6 clo.
@@ -733,6 +774,14 @@ Proof.
   eapply rclo6_clo_base, PR.
 Qed.
 
+Lemma prespect6_companion
+      clo (RES: prespectful6 clo):
+  clo <7= cpn6 gf.
+Proof.
+  intros. eapply compatible'6_companion. apply prespect6_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect6_uclo
       clo (RES: wrespectful6 clo):
   clo <7= gupaco6 gf (cpn6 gf).
@@ -740,6 +789,13 @@ Proof.
   intros. eapply gpaco6_clo, wrespect6_companion, PR. apply RES.
 Qed.
 
+Lemma prespect6_uclo
+      clo (RES: prespectful6 clo):
+  clo <7= gupaco6 gf (cpn6 gf).
+Proof.
+  intros. eapply gpaco6_clo, prespect6_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco6.
@@ -752,3 +808,4 @@ Hint Resolve gpaco6_final : paco.
 Hint Resolve rclo6_base : paco.
 Hint Constructors gpaco6 : paco.
 Hint Resolve wrespect6_uclo : paco.
+Hint Resolve prespect6_uclo : paco.
diff --git a/src/gpaco7.v b/src/gpaco7.v
index 4b5905b..c33f7ae 100644
--- a/src/gpaco7.v
+++ b/src/gpaco7.v
@@ -664,6 +664,17 @@ Structure wrespectful7 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful7.
 
+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);
+    }.
+Hint Constructors prespectful7.
+
 Definition gf'7 := id /8\ gf.
 
 Definition compatible'7 := compatible7 gf'7.
@@ -684,6 +695,36 @@ Proof.
     + intros. apply rclo7_rclo, PR.
 Qed.
 
+Lemma prespect7_compatible'
+      clo (RES: prespectful7 clo):
+  compatible'7 (fun r => upaco7 gf (r \7/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco7_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'7 r \7/ clo (gf'7 r)) <7= (r \7/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco7_mon. apply H. apply LEM.
+    + apply paco7_unfold; [apply gf_mon|].
+      eapply paco7_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco7_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat7_compatible'
       clo (COM: compatible7 gf clo):
   compatible'7 clo.
@@ -734,6 +775,14 @@ Proof.
   eapply rclo7_clo_base, PR.
 Qed.
 
+Lemma prespect7_companion
+      clo (RES: prespectful7 clo):
+  clo <8= cpn7 gf.
+Proof.
+  intros. eapply compatible'7_companion. apply prespect7_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect7_uclo
       clo (RES: wrespectful7 clo):
   clo <8= gupaco7 gf (cpn7 gf).
@@ -741,6 +790,13 @@ Proof.
   intros. eapply gpaco7_clo, wrespect7_companion, PR. apply RES.
 Qed.
 
+Lemma prespect7_uclo
+      clo (RES: prespectful7 clo):
+  clo <8= gupaco7 gf (cpn7 gf).
+Proof.
+  intros. eapply gpaco7_clo, prespect7_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco7.
@@ -753,3 +809,4 @@ Hint Resolve gpaco7_final : paco.
 Hint Resolve rclo7_base : paco.
 Hint Constructors gpaco7 : paco.
 Hint Resolve wrespect7_uclo : paco.
+Hint Resolve prespect7_uclo : paco.
diff --git a/src/gpaco8.v b/src/gpaco8.v
index 70493a9..e6a6224 100644
--- a/src/gpaco8.v
+++ b/src/gpaco8.v
@@ -665,6 +665,17 @@ Structure wrespectful8 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful8.
 
+Structure prespectful8 (clo: rel -> rel) : Prop :=
+  prespect8_intro {
+      prespect8_mon: monotone8 clo;
+      prespect8_respect :
+        forall l r
+               (LE: l <8= r)
+               (GF: l <8= gf r),
+        clo l <8= paco8 gf (r \8/ clo r);
+    }.
+Hint Constructors prespectful8.
+
 Definition gf'8 := id /9\ gf.
 
 Definition compatible'8 := compatible8 gf'8.
@@ -685,6 +696,36 @@ Proof.
     + intros. apply rclo8_rclo, PR.
 Qed.
 
+Lemma prespect8_compatible'
+      clo (RES: prespectful8 clo):
+  compatible'8 (fun r => upaco8 gf (r \8/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco8_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'8 r \8/ clo (gf'8 r)) <8= (r \8/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco8_mon. apply H. apply LEM.
+    + apply paco8_unfold; [apply gf_mon|].
+      eapply paco8_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco8_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat8_compatible'
       clo (COM: compatible8 gf clo):
   compatible'8 clo.
@@ -735,6 +776,14 @@ Proof.
   eapply rclo8_clo_base, PR.
 Qed.
 
+Lemma prespect8_companion
+      clo (RES: prespectful8 clo):
+  clo <9= cpn8 gf.
+Proof.
+  intros. eapply compatible'8_companion. apply prespect8_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect8_uclo
       clo (RES: wrespectful8 clo):
   clo <9= gupaco8 gf (cpn8 gf).
@@ -742,6 +791,13 @@ Proof.
   intros. eapply gpaco8_clo, wrespect8_companion, PR. apply RES.
 Qed.
 
+Lemma prespect8_uclo
+      clo (RES: prespectful8 clo):
+  clo <9= gupaco8 gf (cpn8 gf).
+Proof.
+  intros. eapply gpaco8_clo, prespect8_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco8.
@@ -754,3 +810,4 @@ Hint Resolve gpaco8_final : paco.
 Hint Resolve rclo8_base : paco.
 Hint Constructors gpaco8 : paco.
 Hint Resolve wrespect8_uclo : paco.
+Hint Resolve prespect8_uclo : paco.
diff --git a/src/gpaco9.v b/src/gpaco9.v
index bddefee..d075d04 100644
--- a/src/gpaco9.v
+++ b/src/gpaco9.v
@@ -666,6 +666,17 @@ Structure wrespectful9 (clo: rel -> rel) : Prop :=
     }.
 Hint Constructors wrespectful9.
 
+Structure prespectful9 (clo: rel -> rel) : Prop :=
+  prespect9_intro {
+      prespect9_mon: monotone9 clo;
+      prespect9_respect :
+        forall l r
+               (LE: l <9= r)
+               (GF: l <9= gf r),
+        clo l <9= paco9 gf (r \9/ clo r);
+    }.
+Hint Constructors prespectful9.
+
 Definition gf'9 := id /10\ gf.
 
 Definition compatible'9 := compatible9 gf'9.
@@ -686,6 +697,36 @@ Proof.
     + intros. apply rclo9_rclo, PR.
 Qed.
 
+Lemma prespect9_compatible'
+      clo (RES: prespectful9 clo):
+  compatible'9 (fun r => upaco9 gf (r \9/ clo r)).
+Proof.
+  econstructor.
+  { red; intros. eapply upaco9_mon. apply IN.
+    intros. destruct PR.
+    - left. apply LE, H.
+    - right. eapply RES. apply H. intros. apply LE, PR. }
+
+  intros r.
+  assert (LEM: (gf'9 r \9/ clo (gf'9 r)) <9= (r \9/ clo r)).
+  { intros. destruct PR.
+    - left. apply H.
+    - right. eapply RES. apply H. intros. apply PR.
+  }
+
+  intros. destruct PR.
+  - split.
+    + left. eapply paco9_mon. apply H. apply LEM.
+    + apply paco9_unfold; [apply gf_mon|].
+      eapply paco9_mon. apply H. apply LEM.
+  - split.
+    + right. apply LEM. apply H.
+    + destruct H.
+      * eapply gf_mon. apply H. intros. right. left. apply PR.
+      * apply paco9_unfold; [apply gf_mon|].
+        eapply RES, H; intros; apply PR.
+Qed.
+
 Lemma compat9_compatible'
       clo (COM: compatible9 gf clo):
   compatible'9 clo.
@@ -736,6 +777,14 @@ Proof.
   eapply rclo9_clo_base, PR.
 Qed.
 
+Lemma prespect9_companion
+      clo (RES: prespectful9 clo):
+  clo <10= cpn9 gf.
+Proof.
+  intros. eapply compatible'9_companion. apply prespect9_compatible'. apply RES.
+  right. right. apply PR.
+Qed.
+
 Lemma wrespect9_uclo
       clo (RES: wrespectful9 clo):
   clo <10= gupaco9 gf (cpn9 gf).
@@ -743,6 +792,13 @@ Proof.
   intros. eapply gpaco9_clo, wrespect9_companion, PR. apply RES.
 Qed.
 
+Lemma prespect9_uclo
+      clo (RES: prespectful9 clo):
+  clo <10= gupaco9 gf (cpn9 gf).
+Proof.
+  intros. eapply gpaco9_clo, prespect9_companion, PR. apply RES.
+Qed.
+
 End Respectful.
 
 End GeneralizedPaco9.
@@ -755,3 +811,4 @@ Hint Resolve gpaco9_final : paco.
 Hint Resolve rclo9_base : paco.
 Hint Constructors gpaco9 : paco.
 Hint Resolve wrespect9_uclo : paco.
+Hint Resolve prespect9_uclo : paco.