proposition: Theorem compFold_support_h : forall (A: Set)(B : Type)(eqda : EqDec A)(P : A -> list B -> list B -> Prop)(c : A -> B -> Comp A) (ls1 ls2 ls3 : list B)(a z : A), In z (getSupport (compFold _ c a ls1)) -> P a ls2 (ls1 ++ ls3) -> (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 (ls2 ++ ls1) ls3.
proof: Proof. induction ls1; intuition; simpl in *. intuition; subst. rewrite app_nil_r. trivial. eapply in_getUnique_if in H. eapply in_flatten in H. destruct H. intuition. eapply in_map_iff in H2. destruct H2. intuition. subst. rewrite app_cons_eq. eapply IHls1. eauto. eapply H1. eauto. eauto. intuition. Qed.
imports: FCF.FCF Permutation