diff --git a/examples/congprog.v b/examples/congprog.v
index 7731441..469118b 100644
--- a/examples/congprog.v
+++ b/examples/congprog.v
@@ -193,8 +193,8 @@ rewrite (_ : _ \+ _ = m \+ (x :-> ith k pf \+
 hhauto; rewrite (sepitS (ith k pf)) finE /= indx_ith ltnSn. 
 rewrite /ctab/table !ffunE eqxx; hhauto.
 apply: tableP2 Hct=>// a. 
-- by rewrite !finE ltnS indx_injE; case: ltngtP.
-by rewrite !finE !ffunE indx_injE; case: eqP=>// ->; rewrite ltnn.
+- by rewrite !finE ltnS inj_indxE; case: ltngtP.
+by rewrite !finE !ffunE inj_indxE; case: eqP=>// ->; rewrite ltnn.
 Qed.
 Next Obligation. 
 case=>_ ->; apply: [stepE]=>//= rx hr Er; apply: [stepU]=>//= cl hc Ec. 
diff --git a/examples/llist.v b/examples/llist.v
index 1adba0f..0eae66c 100644
--- a/examples/llist.v
+++ b/examples/llist.v
@@ -158,7 +158,7 @@ elim: l1 l2 p h => [|x1 xt IH] /= l2 p h V.
 - by case=>->->; case/lseq_null.
 case=>q1 /= [h1][E] H; rewrite {}E in H V *.
 case/(lseq_pos (defPt_nullO V))=>x2 [q2][h2][->] /=.
-do 2![case/(cancel V)=>/dynE/jmE<-{}V].
+do 2![case/(cancel V)=>/inj_dyn<-{}V].
 by move=><- /(IH (behead l2) _ _ V H)=>->.
 Qed.
 
diff --git a/examples/quicksort.v b/examples/quicksort.v
index b07be05..a794cbf 100644
--- a/examples/quicksort.v
+++ b/examples/quicksort.v
@@ -158,17 +158,17 @@ rewrite {1}(slice_extrude (fgraph f) (i:=Interval i j)) //=.
 rewrite (perm_on_notin (i:=Interval -oo i) f H); last first.
 - rewrite disjoint_subset; apply/subsetP=>/= z.
   rewrite inE=>Hz; rewrite 2!inE; apply/negP=>Hz2.
-  suff: (z : nat) \notin order.Order.meet (Interval -oo i) (Interval i j).
+  suff: (z : nat) \notin Order.meet (Interval -oo i) (Interval i j).
   - by move/negP; apply; rewrite in_itvI Hz2.
-  rewrite /order.Order.meet /= /order.Order.join /= /order.Order.meet /=.
+  rewrite /Order.meet /= /Order.join /= /Order.meet /=.
   move/ltW: Hij; rewrite bound_leEmeet=>/eqP->.
   by rewrite itv_ge // -leNgt.
 rewrite (perm_on_notin (i:=Interval j +oo) f H); last first.
 - rewrite disjoint_subset; apply/subsetP=>/= z.
   rewrite inE=>Hz; rewrite 3!inE; apply/negP=>Hz2.
-  suff: (z : nat) \notin order.Order.meet (Interval i j) (Interval j +oo).
+  suff: (z : nat) \notin Order.meet (Interval i j) (Interval j +oo).
   - by move/negP; apply; rewrite in_itvI Hz.
-  rewrite /order.Order.meet /= /order.Order.meet /=.
+  rewrite /Order.meet /= /Order.meet /=.
   move: (bound_lex1 j); rewrite bound_leEmeet=>/eqP->.
   move/ltW: Hij; rewrite leEjoin=>/eqP->.
   by rewrite itv_ge // -leNgt.
diff --git a/examples/union_find.v b/examples/union_find.v
index 9626df3..4b2f475 100644
--- a/examples/union_find.v
+++ b/examples/union_find.v
@@ -240,7 +240,7 @@ Lemma tlay_rt x (p : ptr) t r :
         if x == rt t then p = r else (p != x) && (p \in t).
 Proof.
 elim/tree_ind1: t r=>a ts IH r; rewrite tlayE /= => /[dup]/In_find/In_valid V.
-rewrite findPtUn2 // in_tnode; case: eqVneq=>[_ [/inj_pair2]|N] //.
+rewrite findPtUn2 // in_tnode; case: eqVneq=>[_ [/inj_dyn]|N] //.
 case/big_find_someX=>t T /(IH _ T) H; case: ifP H N=>[_ ->|_].
 - by rewrite eqxx // eq_sym =>->.
 by case/andP=>-> H _; case: orP=>//; elim; right; apply/hasPIn; exists t.
diff --git a/htt/model.v b/htt/model.v
index 8c1bb4a..4fc0211 100644
--- a/htt/model.v
+++ b/htt/model.v
@@ -714,7 +714,7 @@ have J : x :-> v \+ j \In read_pre.
 - split; first by rewrite domPtUnE.
   by exists v; rewrite findPtUn.
 exists J=>_ _ [w [->->]].
-rewrite findPtUn //; case=>/inj_pair2 {w}<-.
+rewrite findPtUn //; case=>/inj_dyn {w}<-.
 by apply: H.
 Qed.