Skip to content
Snippets Groups Projects
Verified Commit ba2bdb73 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Switch `inj _` to `inj f`, part 1

Code affected by a00d9bd8.
parent eeef6250
No related branches found
No related tags found
1 merge request!138Revise uses of inj as discussed
......@@ -58,7 +58,7 @@ Section namespace.
intros Hxy a. unfold up_close. rewrite !nclose_eq, !ndot_eq.
unfold nclose_def, ndot_def; rewrite !elem_coPset_suffixes.
intros [qx ->] [qy Hqy].
revert Hqy. by intros [= ?%(inj _)]%positives_flatten_suffix_eq.
revert Hqy. by intros [= ?%(inj encode)]%positives_flatten_suffix_eq.
Qed.
Lemma ndot_preserve_disjoint_l N E x : N ## E N.@x ## E.
......
......@@ -189,8 +189,8 @@ Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) m
f <$> mx Some y x, mx = Some x y f x.
Proof.
destruct mx; simpl; split.
- intros ?%(inj _). eauto.
- intros (? & ->%(inj _) & ?). constructor. done.
- intros ?%(inj Some). eauto.
- intros (? & ->%(inj Some) & ?). constructor. done.
- intros ?%symmetry%equiv_None. done.
- intros (? & ? & ?). done.
Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment