proposition: Lemma exec_sequence : forall (i:inst) (s:state) (i1 i2:inst), i = Scolon i1 i2 -> forall (f1:forall s:state, exec_or_not s i1) (f2:forall s:state, exec_or_not s i2), exec_or_not s i.
proof: Proof. intros i s i1 i2 heq f1 f2. case (f1 s). - intros s1 Hexec1; case (f2 s1). + intros s2 Hexec2; apply (result s i s2). rewrite heq; apply execScolon with s1; assumption. + intros Hnot; apply no_result. rewrite heq. intros s'; red in |- *; intros H; inversion H. elim (Hnot s'). rewrite (exec_det s s1 s2 i1); assumption. - intros Hnot; apply no_result. rewrite heq. intros s' H; inversion H. elim (Hnot s1); assumption. Defined.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction