proposition: Lemma bind_EqDec : forall (A B : Set), Comp B -> (B -> Comp A) -> EqDec A.
proof: Proof. intuition. eapply comp_EqDec. eapply X0. eapply comp_base_exists. eauto. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec