Commit 8c382d56 authored by Ralf Jung's avatar Ralf Jung

make proof of fill_not_value fully automatic

parent 2dda1557
......@@ -181,12 +181,7 @@ Qed.
Lemma fill_not_value e K :
e2v e = None -> e2v (fill K e) = None.
Proof.
intros Hnval. induction K =>/=; try reflexivity.
- done.
- by rewrite IHK /=.
- by rewrite v2v /= IHK /=.
- by rewrite IHK /=.
- by rewrite IHK /=.
intros Hnval. induction K =>/=; by rewrite ?v2v /= ?IHK /=.
Qed.
Lemma fill_not_value2 e K v :
......
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