proposition: Lemma listfilter_in : forall L l i x, L[i]=Some x -> l[i]=Some true -> In x (listfilter L l) .
proof: Proof. induction L. intros. simpl in *. discr. intros. destruct i; simpl in H. simpl. inversion H; subst. destruct l; simpl in *. discr. inversion H0; subst. simpl; left; auto. destruct l; auto. simpl in H0; discr. inversion H0. simpl. destruct b. right. eapply IHL; eauto. eapply IHL; eauto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)