proposition: Theorem getSupport_In_evalDet : forall (A : Set)(c : Comp A) a s, evalDet c s (ca_done a) -> In a (getSupport c).
proof: Proof. intuition. inversion H; clear H; subst. eapply getSupport_In_evalDet_steps; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia