Commit 93d279ac authored by charguer's avatar charguer

fixed_compil

parent 4d335a51
......@@ -143,7 +143,7 @@ Proof.
intros.
exists (make (n - 1) x).
rewrite app_cons_one_r.
apply* cons_make_pred_same.
rewrite* <- make_eq_cons_make_pred.
Qed.
Lemma prefix_snoc_write:
......
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