proposition: Lemma evalDet_step_more_support_preserved : forall (A : Set)(c c' : Comp A) s, evalDet_step c s = (cs_more c' s) -> Permutation (getSupport c) (getSupport c').
proof: Proof. induction c; intuition; simpl in *; try discriminate. subst. case_eq (evalDet_step c s); intuition; rewrite H1 in H0. inversion H0; clear H0; subst. erewrite evalDet_step_done_support_singleton; eauto. simpl. rewrite app_nil_r. rewrite getUnique_NoDup_eq. eapply Permutation_refl. eapply getSupport_NoDup. discriminate. inversion H0; clear H0; subst. simpl. eapply getUnique_Permutation. eapply flatten_Permutation. eapply Permutation_map. eauto. case_eq (shiftOut s n); intuition; rewrite H0 in H. destruct p. inversion H; clear H; subst. assert (n = O). eapply shiftOut_same_inv; eauto. subst. simpl. rewrite shiftOut_0 in H0. inversion H0; clear H0; subst. eapply Permutation_refl. discriminate. inversion H; clear H; subst. simpl. eapply NoDup_Permutation. eapply filter_NoDup. eapply getSupport_NoDup. eapply getUnique_NoDup. intuition. eapply in_getUnique. eapply in_flatten. econstructor. split. eapply in_map_iff. econstructor. split. 2:{ eapply filter_In; eauto. } assert (b x = true). eapply filter_In; eauto. rewrite H0. eauto. simpl. intuition. apply in_getUnique_if in H. eapply in_flatten in H. destruct H. intuition. eapply in_map_iff in H0. destruct H0. intuition. subst. case_eq (b x1); intuition; rewrite H in H1. simpl in *. intuition; subst. eapply filter_In; eauto. simpl in *. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia