proposition: Theorem inCompute_inb : forall (t : btree) (a : A) (l : list bool), In (a, l) (compute_code t) -> inb (leaf a) t.
proof: Proof. intros t; elim t; simpl in |- *; auto. intros a a0 l [H1| H1]; try (case H1; fail). injection H1; intros H2 H3; rewrite H3; auto. intros h H h0 H0 a l H1. case in_app_or with (1 := H1); auto; intros H2. case (proj1 (in_map_iff _ _ _)) with (1 := H2). intros (a1, l1) (Hl1, Ha1); auto. apply innodeL; apply (H a l1). injection Hl1; intros Hl2 Hl3; rewrite <- Hl3; auto. case (proj1 (in_map_iff _ _ _)) with (1 := H2). intros (a1, l1) (Hl1, Ha1); auto. apply innodeR; apply (H0 a l1). injection Hl1; intros Hl2 Hl3; rewrite <- Hl3; auto. Qed.
imports: Coq(ArithRing ListDec)