diff --git a/examples/int_to_Zp.v b/examples/int_to_Zp.v
index 9db02f1..a98f461 100644
--- a/examples/int_to_Zp.v
+++ b/examples/int_to_Zp.v
@@ -45,10 +45,6 @@ Definition eqmodp (x y : int) := modp x = modp y.
 Definition eq_Zmodp (x y : Zmodp) := (x = y).
 Arguments eq_Zmodp /.
 
-(* Axiom (eqp_refl : Reflexive eqmodp). *)
-(* Axiom (eqp_sym : Symmetric eqmodp). *)
-(* Axiom (eqp_trans : Transitive eqmodp). *)
-
 Notation "0" := zero : int_scope.
 Notation "0" := zerop : Zmodp_scope.
 Notation "x == y" := (eqmodp x%int y%int)
diff --git a/examples/nat_ind.v b/examples/nat_ind.v
index ace8f58..b972c27 100644
--- a/examples/nat_ind.v
+++ b/examples/nat_ind.v
@@ -23,14 +23,15 @@ Variables (to_nat : I -> nat) (of_nat : nat -> I).
 
 Hypothesis to_natK : forall x, of_nat (to_nat x) = x.
 Hypothesis of_nat0 : of_nat O = I0.
-Hypothesis of_natS : forall x n, of_nat n = x -> of_nat (S n) = IS x.
+Hypothesis of_natS : forall n, of_nat (S n) = IS (of_nat n).
 
-(* We only need/ (2a,3) which is morally that Nmap is a split injection *)
+(* We only need (2a,3), so it suffices that to_nat is a retraction *)
 Definition RI : Param2a3.Rel I nat :=
  SplitSurj.toParamSym (SplitSurj.Build to_natK).
 
 Definition RI0 : RI I0 O. Proof. exact of_nat0. Qed.
-Definition RIS m n : RI m n -> RI (IS m) (S n). Proof. exact: of_natS. Qed.
+Definition RIS m n : RI m n -> RI (IS m) (S n).
+Proof. by move=> <-; apply: of_natS. Qed.
 
 Trocq Use RI RI0 RIS.
 
diff --git a/examples/peano_bin_nat.v b/examples/peano_bin_nat.v
index 84bb71c..a290253 100644
--- a/examples/peano_bin_nat.v
+++ b/examples/peano_bin_nat.v
@@ -19,7 +19,7 @@ From Trocq_examples Require Import N.
 Set Universe Polymorphism.
 
 (* the best we can do to link these types is (4,4), but
-we only need (2a,3) which is morally that Nmap is a split injection *)
+we only need (2a,3) si ut suffices that N.to_nat is a retraction *)
 Definition RN : Param2a3.Rel N nat :=
  SplitSurj.toParamSym (SplitSurj.Build N.to_natK).