proposition: Theorem find_val_correct1 : forall (c : code) (a : A) (l : list bool), find_val l c = Some a -> In (a, l) c.
proof: Proof. intros c a l; elim c; simpl in |- *; auto. intros; discriminate. intros a0; case a0. intros a1 l0 l1; case (list_eq_dec Bool.bool_dec l l0); auto. intros e H H0; injection H0. intros e1; left; apply f_equal2 with (f := pair (A:=A) (B:=list bool)); auto. Qed.
imports: Coq(Sorting.Permutation)