proposition: Lemma exec_skip : forall (i:inst) (s:state), i = Skip -> exec_or_not s i.
proof: Proof. intros i s heq; exact (result s i s (eq_ind_r (fun j:inst => exec s j s) (execSkip s) heq)). Defined.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction