proposition: Lemma getSupport_In_evalDet_step_more : forall (A : Set)(c c' : Comp A) s s' a, evalDet_step c s = cs_more c' s' -> In a (getSupport c') -> In a (getSupport c).
proof: Proof. induction c; intuition; simpl in *. discriminate. case_eq (evalDet_step c s); intuition; rewrite H2 in H0. inversion H0; clear H0; subst. eapply in_getUnique. eapply in_flatten. exists (getSupport (c0 b)). intuition. eapply in_map_iff. exists b. intuition. eapply getSupport_In_evalDet_step_done; eauto. discriminate. inversion H0; clear H0; subst. simpl in *. apply in_getUnique_if in H1. apply in_flatten in H1. destruct H1; intuition. eapply in_getUnique. eapply in_flatten. exists x. intuition. apply in_map_iff in H1. destruct H1; intuition. subst. eapply in_map_iff. exists x0. intuition. eapply IHc; eauto. eapply in_getAllBvectors. inversion H; clear H; subst. simpl in *. eapply in_getUnique_if in H0. eapply in_flatten in H0. destruct H0. intuition. eapply in_map_iff in H0. destruct H0. intuition. subst. case_eq (b x0); intuition; rewrite H in H1; simpl in *. intuition; subst. eapply filter_In; eauto. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia