Commit f295fc40 authored by Heiko Becker's avatar Heiko Becker

Fix next bug in Coq dev

parent 944ba3ca
......@@ -62,7 +62,6 @@ Proof.
- intros approx_bin_true v v_in_fV.
unfold freeVars in v_in_fV.
apply in_app_or in v_in_fV.
unfold approximatesPrecond in approx_bin_true.
apply Is_true_eq_left in approx_bin_true.
destruct (absenv (Binop b e1 e2)); destruct (absenv e1); destruct (absenv e2); simpl in *.
apply andb_prop_elim in approx_bin_true.
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