proposition: Theorem not_null_find_val : forall c : code, not_null c -> find_val [] c = None.
proof: Proof. intros c; elim c; simpl; auto. intros a; case a. intros a1 l; case (list_eq_dec Bool.bool_dec [] l); auto. intros e l0 H H0; case (H0 a1); rewrite e; simpl in |- *; auto. intros n l0 H H0; apply H. unfold not_null in |- *; intros a2; red in |- *; intros H1. case (H0 a2); simpl in |- *; auto. Qed.
imports: Coq(Sorting.Permutation)