proposition: Lemma getSupport_In_evalDet_step_done : forall (A : Set)(c : Comp A) a s s', evalDet_step c s = cs_done a s' -> In a (getSupport c).
proof: Proof. induction c; intuition; simpl in *. inversion H; clear H; subst. intuition. destruct (evalDet_step c s); try discriminate. eapply in_getAllBvectors. discriminate. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia