proposition: Lemma combine_aux_combine': forall A c prefix brbit t1_1 t1_2 (t2: ptrie A), combine' c (Branch prefix brbit t1_1 t1_2) t2 = ((fix combine_aux (t2 : ptrie A) : ptrie A := match t2 with | Empty => Branch prefix brbit t1_1 t1_2 | Leaf i x => if Key.match_prefix i prefix brbit then if Key.zerobit i brbit then Branch prefix brbit (insert' (fun a b : A => c b a) i x t1_1) t1_2 else Branch prefix brbit t1_1 (insert' (fun a b : A => c b a) i x t1_2) else join i (Leaf i x) prefix (Branch prefix brbit t1_1 t1_2) | Branch p2 m2 l2 r2 => if elt_eqb prefix p2 && elt_eqb brbit m2 then Branch prefix brbit (combine' c t1_1 l2) (combine' c t1_2 r2) else if Key.ltb brbit m2 && Key.match_prefix p2 prefix brbit then if Key.zerobit p2 brbit then Branch prefix brbit (combine' c t1_1 t2) t1_2 else Branch prefix brbit t1_1 (combine' c t1_2 t2) else if Key.ltb m2 brbit && Key.match_prefix prefix p2 m2 then if Key.zerobit prefix m2 then Branch p2 m2 (combine_aux l2) r2 else Branch p2 m2 l2 (combine_aux r2) else join prefix (Branch prefix brbit t1_1 t1_2) p2 t2 end) t2).
proof: Proof. intros; unfold combine'; fold combine'. unfold insert'; fold insert'. reflexivity. Qed.
imports: Lia Cdcl.Coqlib