proposition: Lemma compFold_nop : forall (A: Set)(B : Type)(eqd : EqDec A)(c : A -> B -> Comp A)(ls : list B) init x, In x (getSupport (compFold _ c init ls)) -> (forall b a, In b ls -> In a (getSupport (c init b)) -> a = init) -> x = init.
proof: Proof. induction ls; intuition. simpl in *. intuition. unfold compFold in H. fold compFold in H. simp_in_support. assert (x0 = init). eapply H0; eauto. simpl. intuition. subst. eapply IHls. trivial. intuition. eapply H0; eauto. simpl. intuition. Qed.
imports: FCF.FCF