Commit 22e0ade7 authored by Robbert Krebbers's avatar Robbert Krebbers

Removed unused argument for `map_seq` lemmas.

parent b938e033
Pipeline #15270 passed with stage
in 10 minutes and 56 seconds
......@@ -1975,14 +1975,14 @@ Section map_seq.
- by rewrite IH, Nat.add_succ_r, !insert_union_singleton_l, (assoc_L _).
Qed.
Lemma map_seq_cons_disjoint start xs x :
Lemma map_seq_cons_disjoint start xs :
map_seq (M:=M A) (S start) xs !! start = None.
Proof. rewrite lookup_map_seq_None. lia. Qed.
Lemma map_seq_cons start xs x :
map_seq start (x :: xs) =@{M A} <[start:=x]> (map_seq (S start) xs).
Proof. done. Qed.
Lemma map_seq_snoc_disjoint start xs x :
Lemma map_seq_snoc_disjoint start xs :
map_seq (M:=M A) start xs !! (start+length xs) = None.
Proof. rewrite lookup_map_seq_None. lia. Qed.
Lemma map_seq_snoc start xs x :
......
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