Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
febc4054
Commit
febc4054
authored
Nov 25, 2021
by
Michael Sammler
Browse files
comment
parent
e9cbc3cf
Pipeline
#58114
passed with stage
in 16 minutes and 34 seconds
Changes
1
Pipelines
6
Hide whitespace changes
Inline
Side-by-side
theories/lithium/base.v
View file @
febc4054
...
...
@@ -222,6 +222,7 @@ Proof.
split
=>
//
;
by
apply
nil_length_inv
.
Qed
.
(* TODO: replace with upsteamed version *)
Lemma
take_elem_of
{
A
}
(
x
:
A
)
n
l
:
x
∈
take
n
l
↔
∃
i
,
(
i
<
n
)%
nat
∧
l
!!
i
=
Some
x
.
Proof
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment