proposition: Theorem evalDet_steps_bind_more_h : forall(A B : Set) x y, evalDet_steps x y -> forall (c1 : Comp B)(c2 : B -> Comp A) s c1' s', x = (cs_more c1 s) -> y = (cs_more c1' s') -> evalDet_steps (cs_more (Bind c1 c2) s) (cs_more (Bind c1' c2) s').
proof: Proof. induction 1; intuition; subst. Ltac evalDet_tac1 := match goal with | [H : cs_more _ _ = cs_more _ _ |- _ ] => inversion H; clear H; subst | [|- evalDet_steps ?c ?c ] => econstructor | [H : evalDet_steps (evalDet_step ?c ?s) _ |- evalDet_steps (cs_more (Bind ?c _) ?s) _ ] => inversion H; clear H; subst | [H : (evalDet_step ?c ?s) = _ |- evalDet_steps (cs_more (Bind ?c _) ?s) _ ] => econstructor; simpl | [|- context[match ?x with | cs_done _ _ => _ | cs_eof _ => _ | cs_more _ _ => _ end] ] => case_eq x; intuition end. repeat evalDet_tac1. inversion H0; clear H0; subst. inversion H1; clear H1; subst. econstructor. eauto. simpl. rewrite H3. econstructor. inversion H1; clear H1; subst. econstructor. eauto. simpl. rewrite <- H. eapply IHevalDet_steps. auto. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia