proposition: Theorem in_alphabet_compute_code : forall m t, (forall a : A, In a m -> inb (leaf a) t) -> in_alphabet m (compute_code t).
proof: Proof. intros m; elim m; simpl in |- *; auto. intros a l H t H0; cut (inb (leaf a) t); auto; intros H1. case inb_compute_ex with (1 := H1). intros l1 Hl1; apply in_alphabet_cons with (ca := l1); auto. Qed.
imports: Coq(ArithRing ListDec)