diff --git a/theories/collections.v b/theories/collections.v index 6f4e526e3127119b3688ce7cc10081640443a48e..3a49b8deb7e39928a11456bf7098b49468c1c2e0 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -390,7 +390,7 @@ Section simple_collection. split. - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|]. setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver. - - intros [X []]. induction 1; simpl; [by apply elem_of_union_l |]. + - intros [X [Hx]]. induction Hx; simpl; [by apply elem_of_union_l |]. intros. apply elem_of_union_r; auto. Qed. diff --git a/theories/list.v b/theories/list.v index 59b7bda9e163ca67ae0ac65fc67e7cb712b78b87..ab08c510c7a112db57efdde80a6da8940361405d 100644 --- a/theories/list.v +++ b/theories/list.v @@ -926,7 +926,7 @@ Proof. by destruct n. Qed. Lemma drop_length l n : length (drop n l) = length l - n. Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed. Lemma drop_ge l n : length l ≤ n → drop n l = []. -Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed. +Proof. revert n. induction l; intros [|?]; simpl in *; auto with lia. Qed. Lemma drop_all l : drop (length l) l = []. Proof. by apply drop_ge. Qed. Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l. @@ -2828,7 +2828,7 @@ Section fmap. (∀ x, f x = y) → f <\$> l = replicate (length l) y. Proof. intros; induction l; f_equal/=; auto. Qed. Lemma list_lookup_fmap l i : (f <\$> l) !! i = f <\$> (l !! i). - Proof. revert i. induction l; by intros [|]. Qed. + Proof. revert i. induction l; intros [|n]; by try revert n. Qed. Lemma list_lookup_fmap_inv l i x : (f <\$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y. Proof.