Commit 1519c178 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add lemmas for `≼` of `Cinl` and `Cinr`.

parent 4e176be4
......@@ -189,6 +189,10 @@ Proof.
+ exists (Cinl c); by constructor.
+ exists (Cinr c); by constructor.
Qed.
Lemma Cinl_included a a' : Cinl a Cinl a' a a'.
Proof. rewrite csum_included. naive_solver. Qed.
Lemma Cinr_included b b' : Cinr b Cinr b' b b'.
Proof. rewrite csum_included. naive_solver. Qed.
Lemma csum_includedN n x y :
x {n} y y = CsumBot ( a a', x = Cinl a y = Cinl a' a {n} a')
......
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