proposition: Theorem btree_unique_prefix2 : forall t : btree, distinct_leaves t -> unique_key (compute_code t).
proof: Proof. intros t; elim t; simpl in |- *; auto. intros b H b0 H0 H1. apply unique_key_app; auto. apply unique_key_map; auto. apply H; apply distinct_leaves_l with (1 := H1); auto. intros (a1, b1) (a2, b2); simpl in |- *; auto. apply unique_key_map; auto. apply H0; apply distinct_leaves_r with (1 := H1); auto. intros (a1, b1) (a2, b2); simpl in |- *; auto. intros a b1 c H2 H3. case (proj1 (in_map_iff _ _ _)) with (1 := H2); auto; case (proj1 (in_map_iff _ _ _)) with (1 := H3); auto. intros (a1, l1) (Hl1, Ha1) (a2, l2) (Hl2, Ha2). apply (H1 (leaf a) b b0); auto. injection Hl2; intros HH1 HH2; rewrite <- HH2. apply inCompute_inb with (1 := Ha2). injection Hl1; intros HH1 HH2; rewrite <- HH2. apply inCompute_inb with (1 := Ha1). Qed.
imports: Coq(ArithRing ListDec)