proposition: Theorem cover_in_inb_inb : forall l t1 t2 t3, cover l t1 -> In t2 l -> inb t3 t2 -> inb t3 t1.
proof: Proof. intros l t1 t2 t3 H; generalize t2 t3; elim H; clear H l t1 t2 t3; auto with datatypes. simpl in |- *; intros t t2 t3 [H1| H1]; auto. rewrite H1; auto. case H1. intros l1 l2 t1 t2 t3 H H0 H1 t0 t4 H2 H3. cut (In t0 (t1 :: t2 :: l2)); auto. simpl in |- *; intros [H4| [H4| H4]]; auto with datatypes. apply (H1 (node t1 t2)); simpl in |- *; auto. rewrite H4; auto. apply (H1 (node t1 t2)); simpl in |- *; auto. rewrite H4; auto. apply (H1 t0); simpl in |- *; auto. apply Permutation_in with (1 := H); simpl in |- *; auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)