proposition: Lemma to_list_nil_inv : forall (A : Type)(n : nat)(v : Vector.t A n), Vector.to_list v = nil -> n = O.
proof: Proof. intuition. destruct v; simpl in *. trivial. unfold Vector.to_list in *. discriminate. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia