proposition: Lemma comp_answer_eq_dec : forall (A : Set), eq_dec A -> eq_dec (comp_answer A).
proof: Proof. intuition. unfold eq_dec in *. intuition. destruct a1; destruct a2. destruct (H a a0); subst. left. trivial. right. intuition. inversion H0; clear H0; subst. intuition. right; intuition; discriminate. right; intuition; discriminate. left. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia