diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 468990508e39148a52f07b3b2fe0d4c2c306baa7..08a3e348bdc8a99280edfa0e7f7bbe21d290b181 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -35,7 +35,7 @@ Section proofs.
   Proof. intros ??. by rewrite -own_op. Qed.
   Global Instance cinv_own_as_fractionnal γ q :
     AsFractional (cinv_own γ q) (cinv_own γ) q.
-  Proof. done. Qed.
+  Proof. split. done. apply _. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ✓ (q1 + q2)%Qp.
   Proof. apply (own_valid_2 γ q1 q2). Qed.
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index 98c4a03dfad61ca3873681e9b0775057c5e78c49..cce3c8057cab7271dfe4d73f59ecfda721086cf5 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -5,8 +5,10 @@ From iris.proofmode Require Import classes class_instances.
 
 Class Fractional {M} (Φ : Qp → uPred M) :=
   fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
-Class AsFractional {M} (P : uPred M) (Φ : Qp → uPred M) (q : Qp) :=
-  as_fractional : P ⊣⊢ Φ q.
+Class AsFractional {M} (P : uPred M) (Φ : Qp → uPred M) (q : Qp) := {
+  as_fractional : P ⊣⊢ Φ q;
+  as_fractional_fractional :> Fractional Φ
+}.
 
 Arguments fractional {_ _ _} _ _.
 
@@ -78,11 +80,15 @@ Section fractional.
   (** Mult instances *)
 
   Global Instance mult_fractional_l Φ Ψ p :
-    (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Ψ → Fractional Φ.
-  Proof. intros AF F q q'. by rewrite !AF Qp_mult_plus_distr_l F. Qed.
+    (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Φ.
+  Proof.
+    intros H q q'. rewrite ->!as_fractional, Qp_mult_plus_distr_l. by apply H.
+  Qed.
   Global Instance mult_fractional_r Φ Ψ p :
-    (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Ψ → Fractional Φ.
-  Proof. intros AF F q q'. by rewrite !AF Qp_mult_plus_distr_r F. Qed.
+    (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Φ.
+  Proof.
+    intros H q q'. rewrite ->!as_fractional, Qp_mult_plus_distr_r. by apply H.
+  Qed.
 
   (* REMARK: These two instances do not work in either direction of the
      search:
@@ -91,58 +97,71 @@ Section fractional.
          with the goal does not work. *)
   Instance mult_as_fractional_l P Φ p q :
     AsFractional P Φ (q * p) → AsFractional P (λ q, Φ (q * p)%Qp) q.
-  Proof. done. Qed.
+  Proof.
+    intros H. split. apply H. eapply (mult_fractional_l _ Φ p).
+    split. done. apply H.
+  Qed.
   Instance mult_as_fractional_r P Φ p q :
     AsFractional P Φ (p * q) → AsFractional P (λ q, Φ (p * q)%Qp) q.
-  Proof. done. Qed.
+  Proof.
+    intros H. split. apply H. eapply (mult_fractional_r _ Φ p).
+    split. done. apply H.
+  Qed.
 
   (** Proof mode instances *)
   Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → Fractional Φ →
-    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
+    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
     FromSep P P1 P2.
-  Proof. by rewrite /FromSep=> -> -> -> ->. Qed.
+  Proof. by rewrite /FromSep=>-[-> ->] [-> _] [-> _]. Qed.
   Global Instance from_sep_fractional_bwd P P1 P2 Φ q1 q2 :
-    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → Fractional Φ →
-    AsFractional P Φ (q1 + q2) →
+    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → AsFractional P Φ (q1 + q2) →
     FromSep P P1 P2 | 10.
-  Proof. by rewrite /FromSep=> -> -> <- ->. Qed.
+  Proof. by rewrite /FromSep=>-[-> _] [-> <-] [-> _]. Qed.
 
   Global Instance from_sep_fractional_half_fwd P Q Φ q :
-    AsFractional P Φ q → Fractional Φ →
-    AsFractional Q Φ (q/2) →
+    AsFractional P Φ q → AsFractional Q Φ (q/2) →
     FromSep P Q Q | 10.
-  Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=> -> -> ->. Qed.
+  Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=>-[-> ->] [-> _]. Qed.
   Global Instance from_sep_fractional_half_bwd P Q Φ q :
-    AsFractional P Φ (q/2) → Fractional Φ →
-    AsFractional Q Φ q →
+    AsFractional P Φ (q/2) → AsFractional Q Φ q →
     FromSep Q P P.
-  Proof. rewrite /FromSep=> -> <- ->. by rewrite Qp_div_2. Qed.
+  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
 
   Global Instance into_and_fractional P P1 P2 Φ q1 q2 :
-    AsFractional P Φ (q1 + q2) → Fractional Φ →
-    AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
+    AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
     IntoAnd false P P1 P2.
-  Proof. by rewrite /AsFractional /IntoAnd=>->->->->. Qed.
+  Proof. by rewrite /IntoAnd=>-[-> ->] [-> _] [-> _]. Qed.
   Global Instance into_and_fractional_half P Q Φ q :
-    AsFractional P Φ q → Fractional Φ →
-    AsFractional Q Φ (q/2) →
+    AsFractional P Φ q → AsFractional Q Φ (q/2) →
     IntoAnd false P Q Q | 100.
-  Proof. by rewrite /AsFractional /IntoAnd -{1}(Qp_div_2 q)=>->->->. Qed.
-
-  Global Instance frame_fractional_l R Q PP' QP' Φ r p p' :
-    AsFractional R Φ r → AsFractional PP' Φ (p + p') → Fractional Φ →
-    Frame R (Φ p) Q → MakeSep Q (Φ p') QP' → Frame R PP' QP'.
-  Proof. rewrite /Frame=>->->-><-<-. by rewrite assoc. Qed.
-  Global Instance frame_fractional_r R Q PP' PQ Φ r p p' :
-    AsFractional R Φ r → AsFractional PP' Φ (p + p') → Fractional Φ →
-    Frame R (Φ p') Q → MakeSep (Φ p) Q PQ → Frame R PP' PQ.
+  Proof. by rewrite /IntoAnd -{1}(Qp_div_2 q)=>-[->->][-> _]. Qed.
+
+  (* The instance [frame_fractional] can be tried at all the nodes of
+     the proof search. The proof search then fails almost always on
+     [AsFractional R Φ r], but the slowdown is still noticeable.  For
+     that reason, we factorize the three instances that could ave been
+     defined for that purpose into one. *)
+  Inductive FrameFractionalHyps R Φ RES : Qp → Qp → Prop :=
+  | frame_fractional_hyps_l Q p p' r:
+      Frame R (Φ p) Q → MakeSep Q (Φ p') RES →
+      FrameFractionalHyps R Φ RES r (p + p')
+  | frame_fractional_hyps_r Q p p' r:
+      Frame R (Φ p') Q → MakeSep Q (Φ p) RES →
+      FrameFractionalHyps R Φ RES r (p + p')
+  | frame_fractional_hyps_half p:
+      AsFractional RES Φ (p/2)%Qp → FrameFractionalHyps R Φ RES (p/2)%Qp p.
+  Existing Class FrameFractionalHyps.
+  Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
+         frame_fractional_hyps_half.
+  Global Instance frame_fractional R r Φ P p RES:
+    AsFractional R Φ r → AsFractional P Φ p → FrameFractionalHyps R Φ RES r p →
+    Frame R P RES.
   Proof.
-    rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm.
+    rewrite /Frame=>-[HR _][->?]H.
+    revert H HR=>-[Q p0 p0' r0|Q p0 p0' r0|p0].
+    - rewrite fractional=><-<-. by rewrite assoc.
+    - rewrite fractional=><-<-=>_.
+      rewrite (comm _ Q (Φ p0)) !assoc. f_equiv. by rewrite comm.
+    - move=>-[-> _]->. by rewrite -fractional Qp_div_2.
   Qed.
-  Global Instance frame_fractional_half P Q R Φ p:
-    AsFractional R Φ (p/2) → AsFractional P Φ p → Fractional Φ →
-    AsFractional Q Φ (p/2)%Qp →
-    Frame R P Q.
-  Proof. by rewrite /Frame -{2}(Qp_div_2 p)=>->->->->. Qed.
 End fractional.
diff --git a/theories/prelude/vector.v b/theories/prelude/vector.v
index 3e32c2a691e3d595f085d52df959dea579fe9ac2..4e62f4bcc1a12438045473b0ca4be7a8956d8846 100644
--- a/theories/prelude/vector.v
+++ b/theories/prelude/vector.v
@@ -78,10 +78,12 @@ Qed.
 
 Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
 Proof. induction i; simpl; lia. Qed.
-Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (Fin.of_nat_lt H) = n.
+Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (fin_of_nat H) = n.
 Proof.
   revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia.
 Qed.
+Lemma fin_of_to_nat {n} (i : fin n) H : @fin_of_nat (fin_to_nat i) n H = i.
+Proof. apply (inj fin_to_nat), fin_to_of_nat. Qed.
 
 Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
     (H1 : ∀ i1 : fin n1, P (Fin.L n2 i1))
@@ -258,16 +260,28 @@ Lemma vec_to_list_take_drop_lookup {A n} (v : vec A n) (i : fin n) :
   vec_to_list v = take i v ++ v !!! i :: drop (S i) v.
 Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed.
 
+Lemma vlookup_lookup {A n} (v : vec A n) (i : fin n) x :
+  v !!! i = x ↔ (v : list A) !! (i : nat) = Some x.
+Proof.
+  induction v as [|? ? v IH]; inv_fin i. simpl; split; congruence. done.
+Qed.
+Lemma vlookup_lookup' {A n} (v : vec A n) (i : nat) x :
+  (∃ H : i < n, v !!! (fin_of_nat H) = x) ↔ (v : list A) !! i = Some x.
+Proof.
+  split.
+  - intros [Hlt ?]. rewrite <-(fin_to_of_nat i n Hlt). by apply vlookup_lookup.
+  - intros Hvix. assert (Hlt:=lookup_lt_Some _ _ _ Hvix).
+    rewrite vec_to_list_length in Hlt. exists Hlt.
+    apply vlookup_lookup. by rewrite fin_to_of_nat.
+Qed.
 Lemma elem_of_vlookup {A n} (v : vec A n) x :
   x ∈ vec_to_list v ↔ ∃ i, v !!! i = x.
 Proof.
-  split.
-  - induction v; simpl; [by rewrite elem_of_nil |].
-    inversion 1; subst; [by eexists 0%fin|].
-    destruct IHv as [i ?]; trivial. by exists (FS i).
-  - intros [i ?]; subst. induction v as [|??? IH]; inv_fin i; [by left|].
-    right; apply IH.
+  rewrite elem_of_list_lookup. setoid_rewrite <-vlookup_lookup'.
+  split; [by intros (?&?&?); eauto|]. intros [i Hx].
+  exists i, (fin_to_nat_lt _). by rewrite fin_of_to_nat.
 Qed.
+
 Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) :
   Forall P (vec_to_list v) ↔ ∀ i, P (v !!! i).
 Proof. rewrite Forall_forall. setoid_rewrite elem_of_vlookup. naive_solver. Qed.
diff --git a/theories/program_logic/gen_heap.v b/theories/program_logic/gen_heap.v
index 826a62ddf11807d96af8f8d3f5748e366f8a5c78..a19923ef3b567dddbae688266c8562b18db2ebbd 100644
--- a/theories/program_logic/gen_heap.v
+++ b/theories/program_logic/gen_heap.v
@@ -82,7 +82,7 @@ Section gen_heap.
   Qed.
   Global Instance mapsto_as_fractional l q v :
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
-  Proof. done. Qed.
+  Proof. split. done. apply _. Qed.
 
   Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
   Proof.
@@ -100,7 +100,7 @@ Section gen_heap.
   Qed.
   Global Instance heap_ex_mapsto_as_fractional l q :
     AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
-  Proof. done. Qed.
+  Proof. split. done. apply _. Qed.
 
   Lemma mapsto_valid l q v : l ↦{q} v ⊢ ✓ q.
   Proof.