proposition: Lemma getSupport_In_evalDet_steps_h : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall (c : Comp A) a s s', x = (cs_more c s) -> y = (cs_done a s') -> In a (getSupport c).
proof: Proof. induction 1; intuition; subst. discriminate. inversion H1; clear H1; subst. inversion H0; clear H0; subst. eapply getSupport_In_evalDet_step_done; eauto. eapply getSupport_In_evalDet_step_more. eauto. eapply IHevalDet_steps. eauto. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia