proposition: Lemma refineCorrect : forall d l p, In p (refineList d l) -> In (d :: p) l.
proof: Proof. intros d l p. unfold refineList. rewrite in_map_iff. intros. inversion H; clear H. inversion H0; clear H0. generalize H1; clear H1. rewrite filter_In. intros H0. inversion H0; clear H0. unfold tl in H. destruct x eqn:X. + simpl in H2. inversion H2. + simpl in H2. apply eq_dir_b_eq in H2. subst. auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List