proposition: Theorem find_code_app : forall a l1 l2, not_null l1 -> find_code a (l1 ++ l2) = match find_code a l1 with | [] => find_code a l2 | b1 :: l3 => b1 :: l3 end.
proof: Proof. intros a l1; generalize a; elim l1; simpl in |- *; auto; clear a l1. intros (a1, l1) l H a l2 H1; case (A_eq_dec a a1); auto. generalize H1; case l1; auto. intros H0; case (H0 a1); simpl in |- *; auto. cut (not_null l); simpl in |- *; auto. apply not_null_inv with (1 := H1); auto. Qed.
imports: Coq(Sorting.Permutation)