proposition: Lemma evalDet_step_well_formed_comp_preserved : forall (A : Set)(c : Comp A), well_formed_comp c -> forall c' s s', evalDet_step c s = (cs_more c' s') -> well_formed_comp c'.
proof: Proof. induction 1; intuition; simpl in *. discriminate. case_eq (evalDet_step c1 s); intuition; rewrite H3 in H2; try discriminate. inversion H2; clear H2; subst. eapply H0. eapply getSupport_In_evalDet_step_done; eauto. inversion H2; clear H2; subst. eapply well_formed_Bind. eapply IHwell_formed_comp. eauto. intuition. eapply H0. eapply getSupport_In_evalDet_step_more; eauto. case_eq (shiftOut s n); intuition; rewrite H0 in H; try discriminate. destruct p. inversion H; clear H; subst. econstructor. inversion H1; clear H1; subst. econstructor. trivial. intuition. case_eq (P b0); intuition. econstructor. econstructor. trivial. trivial. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia