Commit aff91eaa authored by Dan Frumin's avatar Dan Frumin
Browse files

Generalize `or_choice_1_r`.

parent 2b04cb3b
......@@ -96,7 +96,7 @@ Section rules.
Qed.
(** Choice on the RHS *)
Lemma or_choice_1_r (e1 e1' e2 : val) A :
Lemma or_choice_1_r (e1 e1' e2 : expr) A :
(REL e1 << e1' : A) -
REL e1 << (e1' e2)%V : A. (* TODO: in the value scope *)
Proof.
......
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