diff --git a/theories/decidable.v b/theories/decidable.v
index 4c4f154ee45138a58fd632b5cc2e1c642c03a658..6d81008143ef100f8a94f00ca615c2435b2e3cae 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -12,6 +12,8 @@ Proof. firstorder. Qed.
 
 Lemma Is_true_reflect (b : bool) : reflect b b.
 Proof. destruct b. by left. right. intros []. Qed.
+Instance: Injective (=) (↔) Is_true.
+Proof. intros [] []; simpl; intuition. Qed.
 
 (** We introduce [decide_rel] to avoid inefficienct computation due to eager
 evaluation of propositions by [vm_compute]. This inefficiency occurs if
@@ -105,10 +107,12 @@ Tactic Notation "case_bool_decide" "as" ident (Hd) :=
 Tactic Notation "case_bool_decide" :=
   let H := fresh in case_bool_decide as H.
 
-Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
+Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P ↔ P.
 Proof. unfold bool_decide. by destruct dec. Qed.
+Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
+Proof. by rewrite bool_decide_spec. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
-Proof. unfold bool_decide. by destruct dec. Qed.
+Proof. by rewrite bool_decide_spec. Qed.
 
 (** * Decidable Sigma types *)
 (** Leibniz equality on Sigma types requires the equipped proofs to be
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b66dcc14fa2a23283046a857f00645bab2634aed..9fcfe103120e1b04ed9472eed3314634b9332ce6 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1342,6 +1342,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
     rewrite lookup_delete in H || rewrite lookup_delete_ne in H by tac
   | H : context[ {[ _ ]} !! _ ] |- _ =>
     rewrite lookup_singleton in H || rewrite lookup_singleton_ne in H by tac
+  | H : context[ (_ <$> _) !! _ ] |- _ => rewrite lookup_fmap in H
   | H : context[ lookup (A:=?A) ?i (?m1 ∪ ?m2) ] |- _ =>
     let x := fresh in evar (x:A);
     let x' := eval unfold x in x in clear x;
@@ -1357,6 +1358,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
     rewrite lookup_delete || rewrite lookup_delete_ne by tac
   | |- context[ {[ _ ]} !! _ ] =>
     rewrite lookup_singleton || rewrite lookup_singleton_ne by tac
+  | |- context[ (_ <$> _) !! _ ] => rewrite lookup_fmap
   | |- context [ lookup (A:=?A) ?i ?m ] =>
     let x := fresh in evar (x:A);
     let x' := eval unfold x in x in clear x;
@@ -1398,6 +1400,9 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
     apply map_union_cancel_r in H; [|by tac|by tac]
   | H : {[?i,?x]} = ∅ |- _ => by destruct (map_non_empty_singleton i x)
   | H : ∅ = {[?i,?x]} |- _ => by destruct (map_non_empty_singleton i x)
+  | H : ?m !! ?i = Some _, H2 : ?m !! ?j = None |- _ =>
+     unless (i ≠ j) by done;
+     assert (i ≠ j) by (by intros ?; simplify_equality)
   end.
 Tactic Notation "simplify_map_equality'" "by" tactic3(tac) :=
   repeat (progress csimpl in * || simplify_map_equality by tac).