proposition: Lemma comp_EqDec : forall (A : Set), Comp A -> EqDec A.
proof: Proof. induction 1; intuition auto with typeclass_instances. exists (fun a1 a2 => if e a1 a2 then true else false). intuition. destruct (e x y); simpl in *; trivial. discriminate. subst. destruct (e y y); trivial; congruence. eapply H. eapply comp_base_exists; eauto. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec