(* SKC-LISP-WORLD: Mutation Validation Gate *)
Require Import Coq.Init.Prelude.
Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Require Import Machine.State.
Require Import Mutation.Event.
Require Import World.ObjectKinds.
Require Import Coq.omega.Omega.
Lemma generation_monotonicity : forall e,
  mutation_gate_valid e = true ->
  generation_before e < generation_after e.
Proof.
  intros e Hvalid.
  unfold mutation_gate_valid in Hvalid.
  simp in Hvalid.
  unfold generation_advances in *.
  cases (generation_after e > generation_before e); try discriminate.
  omega.
Qed.