proposition: Theorem find_code_permutation : forall (a : A) (c1 c2 : code), Permutation c1 c2 -> unique_prefix c1 -> find_code a c1 = find_code a c2.
proof: Proof. intros a c1 c2 H; elim H; simpl in |- *; auto. intros a0; case a0. intros a1; case (A_eq_dec a a1); auto. intros n l L1 L2 H0 H1 H2; apply H1. apply unique_prefix_inv with (1 := H2). intros a0; case a0. intros a1 l1. case (A_eq_dec a a1). intros Ha1 b; case b; auto. intros a2 l2 L HL; case (A_eq_dec a a2); auto. intros e. case unique_key_in with (1 := unique_prefix2 _ HL) (b2 := l1); auto. rewrite <- Ha1; rewrite e; simpl in |- *; auto. intros Ha1 b; case b; auto. intros L1 L2 L3 H0 H1 H2 H3 H4; apply trans_equal with (find_code a L2); auto. apply H3. apply (unique_prefix_permutation _ _ H0); auto. Qed.
imports: Coq(Sorting.Permutation)