Commit 728bf3ba authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Apply suggestion to theories/algebra/agree.v

parent ae1ed016
...@@ -207,7 +207,7 @@ Proof. ...@@ -207,7 +207,7 @@ Proof.
by move=> /agree_op_invN->; rewrite agree_idemp. by move=> /agree_op_invN->; rewrite agree_idemp.
Qed. Qed.
Lemma to_agree_includedN n a b : to_agree a {n}to_agree b a {n} b. Lemma to_agree_includedN n a b : to_agree a {n} to_agree b a {n} b.
Proof. Proof.
split; last by intros ->. split; last by intros ->.
intros (x & Heq). destruct Heq as [_ Hincl]. intros (x & Heq). destruct Heq as [_ Hincl].
......
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