proposition: Lemma exec_app : forall (c c' : code) x s , exec (c ++ c') x s = match exec c x s with | None => None | Some (y,s') => exec c' y s' end.
proof: Proof. induction c; cbn. - trivial. - intros c' x s; destruct a. + destruct s. * auto. * rewrite IHc. auto. + rewrite IHc. auto. + rewrite IHc; auto. + destruct s; auto. * destruct s; auto. Qed.
imports: Coq(List PArith Relations Lia) additions(Monoid_def Monoid_instances Strategies) Coq(Recdef Wf_nat) additions(More_on_positive Pow Euclidean_Chains Dichotomy BinaryStrat)