blocking_semantic: eval_change_free proof

examples/hoare_logic/blocking_semantics3.mlw

@@ -363,16 +363,6 @@ lemma eval_msubst:
 (*     (eval_fmla sigma pi (subst f x v) <-> *)
 (*      eval_fmla sigma (Cons(x, (get_stack v pi)) pi) f) *)
 
-(* lemma eval_same_var_term: *)
-(*   forall t:term, sigma:env, pi:stack, id:ident, v1 v2:value. *)
-(*     eval_term sigma (Cons (id,v1) (Cons (id,v2) pi)) t = *)
-(*     eval_term sigma (Cons (id,v1) pi) t *)
-
-(* lemma eval_same_var: *)
-(*   forall f:fmla, sigma:env, pi:stack, id:ident, v1 v2:value. *)
-(*     eval_fmla sigma (Cons (id,v1) (Cons (id,v2) pi)) f <-> *)
-(*     eval_fmla sigma (Cons (id,v1) pi) f *)
-
 lemma eval_swap_term:
 forall t:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
 id1 <> id2 ->
@@ -392,8 +382,9 @@ lemma eval_swap:
     eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)
 
 lemma eval_swap_2:
-  forall f:fmla, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
+  forall f:fmla, id1 id2:ident, v1 v2:value.
     id1 <> id2 ->
+      forall sigma:env, pi:stack.
     (eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <->
     eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f)
 
@@ -404,8 +395,9 @@ lemma eval_term_change_free :
 
  (* Need it for monotonicity*)
 lemma eval_change_free :
-  forall sigma:env, pi:stack, f:fmla, id:ident, v:value.
+  forall f:fmla, id:ident, v:value.
     fresh_in_fmla id f ->
+      forall sigma:env, pi:stack.
     (eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)
 
 (** [valid_fmla f] is true when [f] is valid in any environment *)