proposition: Lemma refinePreservesPrefixFree : forall d l, PrefixFree l -> PrefixFree (refineList d l).
proof: Proof. intros. induction l. - unfold refineList; constructor. - destruct a eqn:A; subst. * apply prefixFreeEmpty in H. subst. unfold refineList. simpl. constructor. * destruct s eqn:S; destruct d; subst. + unfold refineList; simpl. eapply FreeCons. -- apply IHl. inversion H; auto. -- intros. inversion H; subst; clear H. apply in_map_iff in H0. inversion H0; subst; clear H0. inversion H; subst; clear H. apply filter_In in H2. inversion H2; subst; clear H2. destruct x eqn:X; simpl in *. inversion H0. destruct s eqn:S; simpl in *. pose proof H5 (Left :: l0). eapply H2 in H; auto. simpl. instantiate (1 := p2). instantiate (1:= p1). rewrite H1. auto. inversion H0. + unfold refineList; simpl. apply IHl. inversion H. auto. + unfold refineList; simpl. apply IHl. inversion H. auto. + unfold refineList; simpl. eapply FreeCons. -- apply IHl. inversion H; auto. -- intros. inversion H; subst; clear H. apply in_map_iff in H0. inversion H0; subst; clear H0. inversion H; subst; clear H. apply filter_In in H2. inversion H2; subst; clear H2. destruct x eqn:X; simpl in *. inversion H0. destruct s eqn:S; simpl in *. inversion H0. pose proof H5 (Right :: l0). eapply H2 in H; auto. simpl. instantiate (1 := p2). instantiate (1:= p1). rewrite H1. auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List