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