proposition: Lemma evalDet_steps_done_inv_h : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall (c : Comp A)(a : A) s s', x = (cs_more c s) -> y = (cs_done a s') -> exists c'' s'', evalDet_steps (cs_more c s) (cs_more c'' s'') /\ evalDet_step c'' s'' = (cs_done a s').
proof: Proof. induction 1; intuition; subst. discriminate. inversion H1; clear H1; subst. inversion H0; clear H0; subst. econstructor. econstructor. intuition. destruct (IHevalDet_steps c a s s'); eauto. destruct H0; intuition. exists x. exists x0. intuition. symmetry in H. econstructor. eapply H. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia