proposition: Lemma comp_eq_dec : forall (A : Set), Comp A -> eq_dec A.
proof: Proof. induction 1; intuition. eapply H. eapply comp_base_exists; eauto. specialize (@Bvector_eq_dec n); intuition. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec