diff --git a/theories/tree_borrows/bor_lemmas.v b/theories/tree_borrows/bor_lemmas.v
index 1abdb5c5e6adad29c61640195b6a9f39d000aebb..62f5bdd8688a8330c2368046ee589a52b85f00d2 100644
--- a/theories/tree_borrows/bor_lemmas.v
+++ b/theories/tree_borrows/bor_lemmas.v
@@ -148,7 +148,7 @@ Proof.
   - right; right; auto.
 Qed.
 
-Lemma insert_eqv_strict_rel t t' (ins:item) (tr:tree item) (search:Tprop item)
+Lemma insert_eqv_strict_rel t t' (ins:item) (tr:tree item) (search:item -> Prop)
   {search_dec:forall it, Decision (search it)} :
   ~IsTag t ins ->
   ~IsTag t' ins ->
@@ -180,7 +180,7 @@ Proof.
   eapply insert_false_infer_exists; eauto.
 Qed.
 
-Lemma insert_eqv_rel t t' (ins:item) (tr:tree item) (search:Tprop item)
+Lemma insert_eqv_rel t t' (ins:item) (tr:tree item) (search:item -> Prop)
   {search_dec:forall it, Decision (search it)} :
   ~IsTag t ins ->
   ~IsTag t' ins ->
@@ -193,7 +193,7 @@ Proof.
   - erewrite <- insert_eqv_strict_rel in Strict; assumption.
 Qed.
 
-Lemma insert_eqv_imm_rel t t' (ins:item) (tr:tree item) (search:Tprop item)
+Lemma insert_eqv_imm_rel t t' (ins:item) (tr:tree item) (search:item -> Prop)
   {search_dec:forall it, Decision (search it)} :
   ~IsTag t ins ->
   ~IsTag t' ins ->
@@ -780,7 +780,7 @@ Proof.
 Qed.
 
 Lemma tree_apply_access_only_cares_about_rel
-  {tr} {fn : call_id_set -> rel_pos -> Z * nat -> tree.app item} {cids access_tag range}
+  {tr} {fn : call_id_set -> rel_pos -> Z * nat -> item -> option item} {cids access_tag range}
   {rel1 rel2 : tag -> tag -> rel_pos}
   (Agree : forall tg tg', rel1 tg tg' = rel2 tg tg')
   : join_nodes (map_nodes (fun it => fn cids (rel1 access_tag it.(itag)) range it) tr)
diff --git a/theories/tree_borrows/bor_semantics.v b/theories/tree_borrows/bor_semantics.v
index 8f91539428bdbacdaaee0705dc6ad7ed3f359f80..d0d0c6564bac885a51403e2236b01baac97e07d1 100755
--- a/theories/tree_borrows/bor_semantics.v
+++ b/theories/tree_borrows/bor_semantics.v
@@ -58,7 +58,7 @@ Qed.
                                    ^^^^^^ computation may trigger UB.
                        ^^^^^^ location may be uninitialized *)
 Definition mem_apply_loc {X} (fn : option X -> option X) z
-  : app (gmap loc' X) := fun map =>
+  : gmap loc' X -> option (gmap loc' X) := fun map =>
     new ← fn (map !! z);
     Some (<[z := new]> map).
 
@@ -67,7 +67,7 @@ Definition mem_apply_loc {X} (fn : option X -> option X) z
    If the set of locations you want to access cannot be expressed as a range,
    see [mem_fold_apply]. *)
 Fixpoint mem_apply_locs {X} (fn:option X -> option X) z sz
-  {struct sz} : app (gmap loc' X) := fun map =>
+  {struct sz} : gmap loc' X -> option (gmap loc' X) := fun map =>
   match sz with
   | O => Some map
   | S sz' =>
@@ -89,7 +89,7 @@ Definition mem_enumerate_sat {X} (fn : X -> bool)
    If the set of locations you want to access can be expressed as a range,
    see [mem_apply_loc] which might be easier to reason about. *)
 Fixpoint mem_fold_apply {X} (fn : option X -> option X) locs
-  : app (gmap loc' X) := fun map =>
+  : gmap loc' X -> option (gmap loc' X) := fun map =>
   match locs with
   | [] => Some map
   | z::locs' =>
@@ -102,7 +102,7 @@ Fixpoint mem_fold_apply {X} (fn : option X -> option X) locs
    (optionally uninitialized) permissions to Parentpermissions lifted to the entire
    memory by means of [mem_apply_range']. *)
 Definition mem_apply_range' {X} (fn:option X -> option X) (r:range')
-  : app (gmap loc' X) := mem_apply_locs fn r.1 r.2.
+  : gmap loc' X -> option (gmap loc' X) := mem_apply_locs fn r.1 r.2.
 
 (* The behavior of [mem_apply_range'] is completely specified by
    [mem_apply_range'_spec] and [mem_apply_range'_success_condition].
@@ -166,8 +166,9 @@ Qed.
    In practice we prefer expressing the state machine as [lazy_permission -> option lazy_permission].
    The second can easily be lifted to the first when given the default permission
    (stored in [item]'s [initp] field). *)
-Definition permissions_apply_range' (pdefault:lazy_permission) (range:range') (f:app lazy_permission)
-  : app permissions := fun ps =>
+Definition permissions_apply_range' (pdefault:lazy_permission) (range:range')
+  (f:lazy_permission -> option lazy_permission)
+  : permissions -> option permissions := fun ps =>
   mem_apply_range'
     (fun oldp => f (default pdefault oldp))
     range ps.
@@ -232,15 +233,15 @@ Qed.
 
 Notation IsTag t := (fun it => it.(itag) = t) (only parsing).
 
-Definition HasRootTag t : Tprop (tbranch item) := fun br => IsTag t (root br).
+Definition HasRootTag t : tbranch item -> Prop := fun br => IsTag t (root br).
 Global Instance HasRootTag_dec t it : Decision (HasRootTag t it).
 Proof. rewrite /HasRootTag. solve_decision. Defined.
 
-Definition HasStrictChildTag t' : Tprop (tbranch item) := exists_strict_child (IsTag t').
+Definition HasStrictChildTag t' : tbranch item -> Prop := exists_strict_child (IsTag t').
 Global Instance HasStrictChildTag_dec t' tr : Decision (HasStrictChildTag t' tr).
 Proof. rewrite /HasStrictChildTag. solve_decision. Defined.
 
-Definition HasImmediateChildTag t' : Tprop (tbranch item) := exists_immediate_child (IsTag t').
+Definition HasImmediateChildTag t' : tbranch item -> Prop := exists_immediate_child (IsTag t').
 Global Instance HasImmediateChildTag_dec t' tr : Decision (HasImmediateChildTag t' tr).
 Proof. rewrite /HasImmediateChildTag. solve_decision. Defined.
 
@@ -263,18 +264,18 @@ Proof. rewrite /HasImmediateChildTag. solve_decision. Defined.
    - [tree_contains t' tr]
    - [WF : forall tg, tree_contains tg tr -> tree_unique tg tr]
    which is obviously sufficient. *)
-Definition StrictParentChildIn t t' : Tprop (tree item)
+Definition StrictParentChildIn t t' : tree item -> Prop
   := every_subtree (fun br => (IsTag t (root br)) -> (HasStrictChildTag t' br)).
 Global Instance StrictParentChildIn_dec t t' tr : Decision (StrictParentChildIn t t' tr).
 Proof. rewrite /StrictParentChildIn. solve_decision. Defined.
 
 (* Reflexive closure of [StrictParentChildIn]. *)
-Definition ParentChildIn t t' : Tprop (tree item)
+Definition ParentChildIn t t' : tree item -> Prop
   := fun tr => t = t' \/ StrictParentChildIn t t' tr.
 Global Instance ParentChildIn_dec t t' tr : Decision (ParentChildIn t t' tr).
 Proof. rewrite /ParentChildIn. solve_decision. Defined.
 
-Definition ImmediateParentChildIn t t' : Tprop (tree item)
+Definition ImmediateParentChildIn t t' : tree item -> Prop
   := every_subtree (fun br => (IsTag t (root br)) -> (HasImmediateChildTag t' br)).
 Global Instance ImmediateParentChildIn_dec t t' tr : Decision (ImmediateParentChildIn t t' tr).
 Proof. rewrite /ImmediateParentChildIn. solve_decision. Defined.
@@ -345,7 +346,7 @@ Definition requires_init (rel:rel_pos)
 (* State machine without protector UB.
    Protector UB is handled later in [apply_access_perm]. *)
 Definition apply_access_perm_inner (kind:access_kind) (rel:rel_pos) (isprot:bool)
-  : app permission := fun perm =>
+  : permission -> option permission := fun perm =>
   match kind, rel with
   | AccessRead, Foreign _ =>
       (* Foreign read. Makes [Reserved] conflicted, freezes [Active]. *)
@@ -455,7 +456,7 @@ Proof. rewrite /protector_is_strong. try repeat case_match; solve_decision. Defi
    - trigger the protector if it is active and if the transition performed [_ -> Disabled]
    - update the [initialized] status of the permission. *)
 Definition apply_access_perm kind rel (isprot:bool)
-  : app lazy_permission := fun operm =>
+  : lazy_permission -> option lazy_permission := fun operm =>
   let old := operm.(perm) in
   new ← apply_access_perm_inner kind rel isprot old;
   (* can only become more initialized *)
@@ -474,8 +475,8 @@ Definition apply_access_perm kind rel (isprot:bool)
 
 (* The effect of an access on an item is to apply it to the permissions while
    keeping the metadata (tag, protector, default permission) unchanged. *)
-Definition item_apply_access (fn : rel_pos -> bool -> app lazy_permission) cids rel range
-  : app item := fun it =>
+Definition item_apply_access (fn : rel_pos -> bool -> lazy_permission -> option lazy_permission) cids rel range
+  : item -> option item := fun it =>
   let oldps := it.(iperm) in
   let protected := bool_decide (protector_is_active it.(iprot) cids) in
   newps ← permissions_apply_range' (mkPerm PermLazy it.(initp)) range
@@ -486,8 +487,8 @@ Definition item_apply_access (fn : rel_pos -> bool -> app lazy_permission) cids
    This function filters out strict children to turn any function into a function
    that operates only on nonchildren. *)
 Definition nonchildren_only
-  (fn : rel_pos -> bool -> app lazy_permission)
-  : rel_pos -> bool -> app lazy_permission := fun rel isprot perm =>
+  (fn : rel_pos -> bool -> lazy_permission -> option lazy_permission)
+  : rel_pos -> bool -> lazy_permission -> option lazy_permission := fun rel isprot perm =>
   match rel with
   | Foreign (Parent _) => Some perm
   | _ => fn rel isprot perm
@@ -496,7 +497,7 @@ Definition nonchildren_only
 (* Lift a function on nodes to a function on trees.
    Returns [None] if and only if the image by at least one of the nodes returns [None]. *)
 Definition tree_apply_access
-  (fn:rel_pos -> bool -> app lazy_permission)
+  (fn:rel_pos -> bool -> lazy_permission -> option lazy_permission)
   cids (access_tag:tag) range (tr:tree item)
   : option (tree item) :=
   let app : item -> option item := fun it => (
@@ -551,7 +552,7 @@ Proof.
 Qed.
 
 Definition memory_access_maybe_nonchildren_only b kind cids tg range
-  : app (tree item) := fun tr =>
+  : tree item -> option (tree item) := fun tr =>
   tree_apply_access (maybe_non_children_only b (apply_access_perm kind)) cids tg range tr.
 
 Definition memory_access := memory_access_maybe_nonchildren_only false.
@@ -562,7 +563,7 @@ Definition memory_access_nonchildren_only := memory_access_maybe_nonchildren_onl
    except trigger UB if there is still a protector, but it's simpler to express it
    in terms of functions that we already have. *)
 Definition memory_deallocate cids t range
-  : app (tree item) := fun tr =>
+  : tree item -> option (tree item) := fun tr =>
   (* Implicit write on deallocation. *)
   let post_write := memory_access AccessWrite cids t range tr in
   (* Then strong protector UB. *)
@@ -797,7 +798,7 @@ Definition create_new_item tg pk rk (cid : call_id) :=
   {| itag:=tg; iprot:=prot; initp:=perm; iperm:=∅ |}.
 
 Definition create_child cids (oldt:tag) (newt:tag) pk rk (cid : call_id)
-  : app (tree item) := fun tr =>
+  : tree item -> option (tree item) := fun tr =>
   let it := create_new_item newt pk rk cid in
   Some $ insert_child_at tr it (IsTag oldt).
 
@@ -808,13 +809,13 @@ Definition item_perm_at_loc it z
   : permission :=
   perm (item_lazy_perm_at_loc it z).
 
-Definition every_tagged t (P:Tprop item) tr
+Definition every_tagged t (P:item -> Prop) tr
   : Prop :=
   every_node (fun it => IsTag t it -> P it) tr.
 
 (* FIXME: gmap::partial_alter ? *)
-Definition apply_within_trees (fn:app (tree item)) blk
-  : app trees := fun trs =>
+Definition apply_within_trees (fn:tree item -> option (tree item)) blk
+  : trees -> option trees := fun trs =>
   oldtr ← trs !! blk;
   newtr ← fn oldtr;
   Some $ <[blk := newtr]> trs.
@@ -899,12 +900,12 @@ Definition tree_get_all_protected_tags_initialized_locs (cid : nat) (tr : tree i
   ) tr.
 
 Definition tree_read_all_protected_initialized (cids : call_id_set) (cid : nat)
-    : app (tree item) := fun tr =>
+  : tree item -> option (tree item) := fun tr =>
     (* read one loc by doing a memory_access *)
-    let reader_loc (tg : tag) (loc : Z) : app (tree item) := fun tr =>
+    let reader_loc (tg : tag) (loc : Z) : tree item -> option (tree item) := fun tr =>
       memory_access_nonchildren_only AccessRead cids tg (loc, 1) tr in
     (* read several locs of the same tag, propagate failures *)
-    let reader_locs (tg : tag) (locs : gset Z) : app (tree item) := fun tr =>
+    let reader_locs (tg : tag) (locs : gset Z) : tree item -> option (tree item) := fun tr =>
       set_fold (fun loc (tr:option (tree item)) => tr ← tr; reader_loc tg loc tr) (Some tr) locs in
     (* get all initialized locs as defined above, these are what we need to read *)
     let init_locs := tree_get_all_protected_tags_initialized_locs cid tr in
diff --git a/theories/tree_borrows/disjoint.v b/theories/tree_borrows/disjoint.v
index efe64aaf30c6699d84c978139a75b4e56537f40a..8b1db1bbf6d1f361c78a3afcfccd58a03f4f6a62 100644
--- a/theories/tree_borrows/disjoint.v
+++ b/theories/tree_borrows/disjoint.v
@@ -1696,7 +1696,7 @@ Proof.
 Qed.
 
 Lemma join_map_commutes
-  {fn1 fn2 : call_id_set -> rel_pos -> Z * nat -> tree.app item} {cids access_tag1 access_tag2 range1 range2}
+  {fn1 fn2 : call_id_set -> rel_pos -> Z * nat -> item -> option item} {cids access_tag1 access_tag2 range1 range2}
   (Fn1PreservesTag : forall it it' cids rel range, fn1 cids rel range it = Some it' -> itag it = itag it')
   (Fn2PreservesTag : forall it it' cids rel range, fn2 cids rel range it = Some it' -> itag it = itag it')
   (Commutes : forall rel1 rel2, commutes
@@ -1738,7 +1738,7 @@ Proof.
 Qed.
 
 Lemma tree_apply_access_only_cares_about_rel
-  {tr} {fn : call_id_set -> rel_pos -> Z * nat -> tree.app item} {cids access_tag range}
+  {tr} {fn : call_id_set -> rel_pos -> Z * nat -> item -> option item} {cids access_tag range}
   {tr1 tr2}
   (Agree : forall tg tg', ParentChildIn tg tg' tr1 <-> ParentChildIn tg tg' tr2)
   (RAgree : forall tg tg', ImmediateParentChildIn tg tg' tr1 <-> ImmediateParentChildIn tg tg' tr2)
diff --git a/theories/tree_borrows/steps_preserve.v b/theories/tree_borrows/steps_preserve.v
index 741895cdbacd72ffb143a65b5537665f3de4474a..6b2dbc1e5dead1a60f1a49abd7bb8f70f87b7c09 100644
--- a/theories/tree_borrows/steps_preserve.v
+++ b/theories/tree_borrows/steps_preserve.v
@@ -5,7 +5,7 @@ From iris.prelude Require Import options.
 (* Any function that operates only on permissions (which is all transitions steps)
    leaves the tag and protector unchanged which means that most of the preservation lemmas
    are trivial once we get to the level of items *)
-Definition preserve_item_metadata (fn:app item) :=
+Definition preserve_item_metadata (fn:item -> option item) :=
   forall it it', fn it = Some it' -> it.(itag) = it'.(itag) /\ it.(iprot) = it'.(iprot) /\ it.(initp) = it'.(initp).
 
 Lemma item_apply_access_preserves_metadata_dep
diff --git a/theories/tree_borrows/steps_wf.v b/theories/tree_borrows/steps_wf.v
index 26a7f2547900ff8d3326bee7e01af887487ad386..0728c65596039b09adc742e939ddebd90fd49fc7 100755
--- a/theories/tree_borrows/steps_wf.v
+++ b/theories/tree_borrows/steps_wf.v
@@ -111,10 +111,10 @@ Proof.
   lia.
 Qed.
 
-Definition preserve_tree_compat_nexts (fn:app (tree item)) nxtp nxtp' nxtc nxtc' :=
+Definition preserve_tree_compat_nexts (fn:tree item -> option (tree item)) nxtp nxtp' nxtc nxtc' :=
   forall tr tr', tree_items_compat_nexts tr nxtp nxtc -> fn tr = Some tr' -> tree_items_compat_nexts tr' nxtp' nxtc'.
 
-Definition preserve_tree_tag_count (fn:app (tree item)) :=
+Definition preserve_tree_tag_count (fn:tree item -> option (tree item)) :=
   forall tr tr' tg, fn tr = Some tr' -> tree_count_tg tg tr = tree_count_tg tg tr'.
 
 Lemma preserve_tag_count_wf fn tr tr' :
diff --git a/theories/tree_borrows/tree.v b/theories/tree_borrows/tree.v
index c1d3e8b102d16172755de6983a8633f5e83c55bc..6e95740ece29182fa3c5f1f5805b501a7d866bad 100644
--- a/theories/tree_borrows/tree.v
+++ b/theories/tree_borrows/tree.v
@@ -3,9 +3,6 @@ From iris.prelude Require Import options.
 
 Implicit Type (V W X Y:Type).
 
-Definition app X : Type := X -> option X.
-Definition Tprop X : Type := X -> Prop.
-
 (** General Preliminaries *)
 
 #[global]
@@ -85,29 +82,29 @@ Definition join_nodes {X}
     Some $ branch data sibling child
   end.
 
-Definition every_subtree {X} (prop:Tprop (tbranch X)) (tr:tree X)
+Definition every_subtree {X} (prop:tbranch X -> Prop) (tr:tree X)
   := fold_subtrees True (fun sub lt rt => prop sub /\ lt /\ rt) tr.
 Global Instance every_subtree_dec {X} prop (tr:tree X) : (forall x, Decision (prop x)) -> Decision (every_subtree prop tr).
 Proof. intro. induction tr; solve_decision. Defined.
 
-Definition exists_subtree {X} (prop:Tprop (tbranch X)) (tr:tree X)
+Definition exists_subtree {X} (prop:tbranch X -> Prop) (tr:tree X)
   := fold_subtrees False (fun sub lt rt => prop sub \/ lt \/ rt) tr.
 Global Instance exists_subtree_dec {X} prop (tr:tree X) : (forall x, Decision (prop x)) -> Decision (exists_subtree prop tr).
 Proof. intro. induction tr; solve_decision. Defined.
 
-Definition every_node {X} (prop:Tprop X) (tr:tree X) := fold_nodes True (fun data lt rt => prop data /\ lt /\ rt) tr.
+Definition every_node {X} (prop:X -> Prop) (tr:tree X) := fold_nodes True (fun data lt rt => prop data /\ lt /\ rt) tr.
 Global Instance every_node_dec {X} prop (tr:tree X) : (forall x, Decision (prop x)) -> Decision (every_node prop tr).
 Proof. intro. induction tr; solve_decision. Defined.
 
-Definition exists_node {X} (prop:Tprop X) (tr:tree X) := fold_nodes False (fun data lt rt => prop data \/ lt \/ rt) tr.
+Definition exists_node {X} (prop:X -> Prop) (tr:tree X) := fold_nodes False (fun data lt rt => prop data \/ lt \/ rt) tr.
 Global Instance exists_node_dec {X} prop (tr:tree X) : (forall x, Decision (prop x)) -> Decision (exists_node prop tr).
 Proof. intro. induction tr; solve_decision. Defined.
 
 Definition count_nodes {X} (prop:X -> bool) :=
   fold_nodes 0 (fun data lt rt => (if prop data then 1 else 0) + lt + rt).
 
-Definition exists_strict_child {X} (prop:Tprop X)
-  : Tprop (tbranch X) := fun '(_, _, child) => exists_node prop child.
+Definition exists_strict_child {X} (prop:X -> Prop)
+  : tbranch X -> Prop := fun '(_, _, child) => exists_node prop child.
 Global Instance exists_strict_child_dec {X} prop (tr:tbranch X) :
   (forall u, Decision (prop u)) -> Decision (exists_strict_child prop tr).
 Proof. intro. solve_decision. Defined.
@@ -117,7 +114,7 @@ Definition empty_children {X} (tr:tbranch X)
   let '(_, _, children) := tr in
   children = empty.
 
-Definition insert_child_at {X} (tr:tree X) (ins:X) (search:Tprop X) {search_dec:forall x, Decision (search x)} : tree X :=
+Definition insert_child_at {X} (tr:tree X) (ins:X) (search:X -> Prop) {search_dec:forall x, Decision (search x)} : tree X :=
   (fix aux tr : tree X :=
     match tr with
     | empty => empty
@@ -142,7 +139,7 @@ Definition exists_sibling {X} (prop:X -> Prop) :=
 Global Instance exists_sibling_dec {X} prop (tr:tree X) : (forall x, Decision (prop x)) -> Decision (exists_sibling prop tr).
 Proof. intro. induction tr; solve_decision. Defined.
 Definition exists_immediate_child {X} (prop:X -> Prop)
-  : Tprop (tbranch X) := fun '(_, _, child) => exists_sibling prop child.
+  : tbranch X -> Prop := fun '(_, _, child) => exists_sibling prop child.
 Global Instance exists_immediate_child_dec {X} prop (tr:tbranch X) :
   (forall u, Decision (prop u)) -> Decision (exists_immediate_child prop tr).
 Proof. intro. solve_decision. Defined.
diff --git a/theories/tree_borrows/tree_lemmas.v b/theories/tree_borrows/tree_lemmas.v
index 2041258b29016e8b6d811452dde8d81f50b1850e..a3cb2394c06255700b776b34bf4452773c7e2064 100644
--- a/theories/tree_borrows/tree_lemmas.v
+++ b/theories/tree_borrows/tree_lemmas.v
@@ -212,7 +212,7 @@ Proof.
   tauto.
 Qed.
 
-Lemma every_not_eqv_not_exists {X} (prop:Tprop X) (tr:tree X) :
+Lemma every_not_eqv_not_exists {X} (prop:X -> Prop) (tr:tree X) :
   every_node (compose not prop) tr
   <-> ~exists_node prop tr.
 Proof.
@@ -268,7 +268,7 @@ Proof.
 Qed.
 *)
 
-Lemma insert_true_preserves_every {X} (tr:tree X) (ins:X) (search prop:Tprop X)
+Lemma insert_true_preserves_every {X} (tr:tree X) (ins:X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   prop ins ->
   every_node prop tr <-> every_node prop (insert_child_at tr ins search).
@@ -287,7 +287,7 @@ Proof.
   inversion H2 as [HIns [H2' HE]]; auto.
 Qed.
 
-Lemma insert_never_unchanged {X} (tr:tree X) (ins:X) (search prop:Tprop X)
+Lemma insert_never_unchanged {X} (tr:tree X) (ins:X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   every_node (compose not search) tr ->
   insert_child_at tr ins search = tr.
@@ -300,7 +300,7 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma insert_preserves_exists {X} (ins:X) (tr:tree X) (search prop:Tprop X)
+Lemma insert_preserves_exists {X} (ins:X) (tr:tree X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   exists_node prop tr -> exists_node prop (insert_child_at tr ins search).
 Proof.
@@ -313,7 +313,7 @@ Proof.
   right; right; right; left; auto.
 Qed.
 
-Lemma exists_sibling_insert {X} (ins:X) (tr:tree X) (search prop:Tprop X)
+Lemma exists_sibling_insert {X} (ins:X) (tr:tree X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   exists_sibling prop tr ↔ exists_sibling prop (insert_child_at tr ins search).
 Proof.
@@ -322,7 +322,7 @@ Proof.
   all: rewrite IHtr1 //.
 Qed.
 
-Lemma insert_false_infer_exists {X} (ins:X) (tr:tree X) (search prop:Tprop X)
+Lemma insert_false_infer_exists {X} (ins:X) (tr:tree X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   ~prop ins ->
   exists_node prop (insert_child_at tr ins search) ->
@@ -340,7 +340,7 @@ Proof.
   - contradiction Ex22.
 Qed.
 
-Lemma insert_true_produces_exists {X} (ins:X) (tr:tree X) (search prop:Tprop X)
+Lemma insert_true_produces_exists {X} (ins:X) (tr:tree X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   prop ins ->
   exists_node search tr ->
@@ -371,7 +371,7 @@ Proof.
 Qed.
 *)
 
-Lemma exists_insert_requires_parent {X} (ins:X) (search prop:Tprop X)
+Lemma exists_insert_requires_parent {X} (ins:X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   forall tr,
   every_node (compose not prop) tr ->
@@ -387,7 +387,7 @@ Proof.
   contradiction.
 Qed.
 
-Lemma remove_false_preserves_exists {X} (ins:X) (search prop:Tprop X)
+Lemma remove_false_preserves_exists {X} (ins:X) (search prop:X -> Prop)
   {search_dec:forall x, Decision (search x)} :
   ~prop ins ->
   forall tr,
@@ -505,7 +505,7 @@ Proof.
   try repeat split; eassumption.
 Qed.
 
-Lemma exists_node_increasing {X} (prop prop':Tprop X) tr :
+Lemma exists_node_increasing {X} (prop prop':X -> Prop) tr :
   exists_node prop tr ->
   every_node (fun x => prop x -> prop' x) tr ->
   exists_node prop' tr.
@@ -517,7 +517,7 @@ Proof.
   - right; right; apply IHtr2; auto.
 Qed.
 
-Lemma every_node_increasing {X} (prop prop':Tprop X) tr :
+Lemma every_node_increasing {X} (prop prop':X -> Prop) tr :
   every_node prop tr ->
   every_node (fun x => prop x -> prop' x) tr ->
   every_node prop' tr.
@@ -529,7 +529,7 @@ Proof.
   exact Ex.
 Qed.
 
-Lemma join_map_preserves_exists {X} (tr tr':tree X) (prop:Tprop X) :
+Lemma join_map_preserves_exists {X} (tr tr':tree X) (prop:X -> Prop) :
   forall fn,
   (forall x y, fn x = Some y -> prop x <-> prop y) ->
   join_nodes (map_nodes fn tr) = Some tr' ->
@@ -547,7 +547,7 @@ Proof.
   tauto.
 Qed.
 
-Lemma join_map_preserves_exists_sibling {X} (tr tr':tree X) (prop:Tprop X) :
+Lemma join_map_preserves_exists_sibling {X} (tr tr':tree X) (prop:X -> Prop) :
   forall fn,
   (forall x y, fn x = Some y -> prop x <-> prop y) ->
   join_nodes (map_nodes fn tr) = Some tr' ->
diff --git a/theories/tree_borrows/trees_equal.v b/theories/tree_borrows/trees_equal.v
index c0d41f2931a94389c0d9a201561ab8341fd075e5..f3ac4613c2935206fa7f93f1fbd22143c82d139e 100644
--- a/theories/tree_borrows/trees_equal.v
+++ b/theories/tree_borrows/trees_equal.v
@@ -714,7 +714,7 @@ Qed.
     (Rel : exists x, rel_dec tr acc_tg tg = Child x)
     : False.
   Proof.
-    inversion Frz as [?? Rel' Lkup Perm].
+    inversion Frz as [it_witness ? Rel' Lkup Perm].
     rewrite -apply_access_success_condition in Acc.
     rewrite every_node_iff_every_lookup in Acc. 2: {
       intros tg0 Ex0. apply unique_lookup. apply GloballyUnique. assumption.
@@ -775,7 +775,7 @@ Qed.
       |???? Prot Confl1 Confl2 Lookup1 Lookup2
       |???? Prot Lookup1 Lookup2
       |witness_tg ?? Dis1 Dis2 Lookup1 Lookup2
-      |???? witness_tg Frz1 Frz2 Lookup1 Lookup2
+      |ini ??? witness_tg Frz1 Frz2 Lookup1 Lookup2
     ].
     - rewrite Tg2 -Tg1.
       rewrite -SameRel.