Commit f7b19ca1 authored by charguer's avatar charguer

normally_val

parent 028fc1a6
......@@ -1401,6 +1401,16 @@ Proof using.
{ exists~ hx hb. splits~. split~. } }
Qed.
Lemma rule_val : forall v H Q,
H ==> Q v ->
triple (trm_val v) (normally H) Q.
Proof using.
introv M. intros h1 h2 D P1. destruct P1 as (P1&E1).
exists h1 v. splits~.
{ applys red_val. }
{ specializes M P1. applys~ on_rw_sub_base. }
Qed.
Definition normal' H :=
(H ==> normally H).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment