Do not unfold compose to prove invert_selfCompose. Instead, use the following lemma:

Lemma selfCompose_succ_alt {A : Type}: forall (f : A -> A) (n : nat),
    f ∘ selfCompose f n ~= selfCompose f n ∘ f.
Admitted.

We found the following function helpful to define insert:

Fixpoint build_singleton {A} (k : list bool) (v : option A) : bitwise_trie A :=
  match k with
  | [] => Node Leaf v Leaf
  | x :: k' =>
      let branch := build_singleton k' v in
      if x then Node branch None Leaf
      else Node Leaf None branch
  end.

The following lemma helps with lookup_insert:

Lemma lookup_build_singleton : forall {A} (k : list bool) (v : option A),
    lookup k (build_singleton k v) = v.
Admitted.

You may find the following lemmas helpful:

Lemma merge_id {A} : forall (t1 : bitwise_trie A),
    merge t1 t1 = t1.
Admitted.

Lemma merge_idempotent {A} : forall (t1 t2 : bitwise_trie A),
    merge t1 (merge t1 t2) = merge t1 t2.
Admitted.

The following lemma is one way to prove bst_implies:

Lemma tree_forall_implies:
  forall tr (P Q: Z -> Prop),
    tree_forall P tr ->
    (forall x, P x -> Q x) ->
    tree_forall Q tr.
Admitted.