proposition: Lemma refineCorrect' : forall d l p, In (d :: p) l -> In p (refineList d l).
proof: Proof. intros. unfold refineList. apply in_map_iff. exists (d :: p). split; auto. apply filter_In. split; simpl; auto. unfold eq_dir_b; destruct d; auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List