proposition: Lemma length_nz_exists : forall (A : Type)(ls : list A), length ls > 0 -> exists a, In a ls.
proof: Proof. destruct ls; intuition; simpl in *. exfalso. eapply lt_eq_false; eauto. econstructor; eauto. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec