proposition: Lemma exec_assign : forall (i:inst) (s:state) (v:Var) (e:aExp), i = Assign v e -> exec_or_not s i.
proof: Proof. intros i s v e heq; case_eq (evalA s e). - intros v' heqa; case_eq (update s v v'). + intros s' Hequ; apply (result s i s'). rewrite heq. apply execAssign with v'; assumption. + intros heq_None; apply no_result. rewrite heq; intros s' H; inversion H. rewrite heqa in H3; injection H3. intros heqv'; rewrite heqv' in heq_None; rewrite H5 in heq_None. discriminate. - intros heq_None; apply no_result. rewrite heq; intros s' H; inversion H. rewrite H3 in heq_None; discriminate. Defined.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction