proposition: Theorem find_code_correct2 : forall (c : code) (a : A) (l : list bool), unique_key c -> In (a, l) c -> find_code a c = l.
proof: Proof. intros c a l; generalize a l; elim c; clear a l c; simpl in |- *; auto. intros a l H H0; case H0. intros a; case a. intros a0 l l0 H a1 l1 H0 H1; case (A_eq_dec a1 a0). intros H2; case H1; intros H3. injection H3; auto. apply unique_key_in_inv with (l := (a0, l) :: l0) (a := a0); simpl in |- *; auto. rewrite <- H2; auto. intros H2; case H1; auto. intros H3; case H2; injection H3; auto. intros; apply H; auto. apply unique_key_inv with (1 := H0); auto. Qed.
imports: Coq(Sorting.Permutation)