proposition: Theorem btree_unique_prefix1 : forall (t : btree) (a1 a2 : A) (lb1 lb2 : list bool), In (a1, lb1) (compute_code t) -> In (a2, lb2) (compute_code t) -> is_prefix lb1 lb2 -> a1 = a2.
proof: Proof. intros t; elim t; simpl in |- *. intros leaf1 a1 a2 lb1 lb2 H1 H2. case H1; intros H3; [ injection H3 | case H3 ]. case H2; intros H4; [ injection H4 | case H4 ]. intros H H0 H5 H6 H7; apply trans_equal with (2 := H0); auto. intros t1 Rec1 t2 Rec2 a1 a2 lb1 lb2 H1 H2. case (in_app_or _ _ _ H1); case (in_app_or _ _ _ H2); clear H1 H2; intros H2 H1 H3. generalize H1 H2; inversion H3. intros H4; case (proj1 (in_map_iff _ _ _)) with (1 := H4). intros x; case x; intros x1 x2 (H6, H5); discriminate. intros H5 H6; apply Rec1 with (lb1 := l1) (lb2 := l2); auto. case (proj1 (in_map_iff _ _ _)) with (1 := H5). intros x; case x. intros a l (H8, H7); injection H8. intros R1 R2 R3; rewrite <- R1; rewrite <- R3; auto. case (proj1 (in_map_iff _ _ _)) with (1 := H6). intros x; case x. intros a l (H8, H7); injection H8. intros R1 R2 R3; rewrite <- R1; rewrite <- R3; auto. generalize H3. case (proj1 (in_map_iff _ _ _)) with (1 := H1). intros x; case x; intros aa1 ll1 (H5, H4). case (proj1 (in_map_iff _ _ _)) with (1 := H2). intros x1; case x1; intros aa2 ll2 (H7, H6). inversion H5; inversion H7; intros tH8; inversion tH8. generalize H3. case (proj1 (in_map_iff _ _ _)) with (1 := H1). intros x; case x; intros aa1 ll1 (H5, H4). case (proj1 (in_map_iff _ _ _)) with (1 := H2). intros x1; case x1; intros aa2 ll2 (H7, H6). inversion H5; inversion H7; intros tH8; inversion tH8. generalize H1 H2; inversion H3. intros H4; case (proj1 (in_map_iff _ _ _)) with (1 := H4). intros x; case x; intros x1 x2 (H6, H5); discriminate. intros H5 H6; apply Rec2 with (lb1 := l1) (lb2 := l2); auto. case (proj1 (in_map_iff _ _ _)) with (1 := H5). intros x; case x. intros a l (H8, H7); injection H8. intros R1 R2 R3; rewrite <- R1; rewrite <- R3; auto. case (proj1 (in_map_iff _ _ _)) with (1 := H6). intros x; case x. intros a l (H8, H7); injection H8. intros R1 R2 R3; rewrite <- R1; rewrite <- R3; auto. Qed.
imports: Coq(ArithRing ListDec)