proposition: Theorem compFold_support : forall (A: Set)(B : Type)(eqda : EqDec A)(P : A -> list B -> list B -> Prop)(c : A -> B -> Comp A) (ls1 : list B)(a z : A), In z (getSupport (compFold _ c a ls1)) -> P a nil ls1 -> (forall a1 a2 b ls1 ls2, In a2 (getSupport (c a1 b)) -> P a1 ls1 (b :: ls2) -> P a2 (ls1 ++ (b :: nil)) ls2 ) -> P z ls1 nil.
proof: Proof. intuition. eapply (compFold_support_h _ P c ls1 nil nil); intuition. eauto. rewrite app_nil_r. trivial. Qed.
imports: FCF.FCF Permutation