proposition: Lemma getSupport_In_evalDet_steps : forall (A : Set)(c : Comp A) a s s', evalDet_steps (cs_more c s) (cs_done a s') -> In a (getSupport c).
proof: Proof. intuition. eapply getSupport_In_evalDet_steps_h; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia