proposition: Theorem find_val_correct2 : forall (c : code) (a : A) (l : list bool), unique_prefix c -> In (a, l) c -> find_val l c = Some a.
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 (list_eq_dec Bool.bool_dec l1 l). intros H2; apply f_equal with (f := Some (A:=A)). case H1; intros H3. injection H3; auto. apply unique_prefix1 with (1 := H0) (lb1 := l) (lb2 := l1); simpl in |- *; auto. rewrite H2; auto. intros H2; case H1; auto. intros H3; case H2; injection H3; auto. intros; apply H; auto. apply unique_prefix_inv with (1 := H0); auto. Qed.
imports: Coq(Sorting.Permutation)