Commit 9a04511b authored by Ralf Jung's avatar Ralf Jung
Browse files

shorten proof

parent c07a5eec
......@@ -1144,8 +1144,7 @@ Section prod.
core (a, b) = (core a, core b).
rewrite /core /core' {1}/pcore /=.
rewrite (cmra_pcore_core a). simpl.
rewrite (cmra_pcore_core b). done.
rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
Global Instance prod_cmra_total : CmraTotal A CmraTotal B CmraTotal prodR.
Supports Markdown
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