Fix list_fmap_inj_1
list_fmap_inj_1
introduced by !344 (merged) accidentally has a superfluous (?A → ?B)
due to Set Default Proof Using "Type*".
:
Check list_fmap_inj_1.
=> list_fmap_inj_1
: (?A → ?B)
→ ∀ (f1 f2 : ?A → ?B) (l : list ?A) (x : ?A),
f1 <$> l = f2 <$> l → x ∈ l → f1 x = f2 x
This MR fixes this such that list_fmap_inj_1
has the intended type:
Check list_fmap_inj_1.
=> list_fmap_inj_1
: ∀ (f f' : ?A → ?B) (l : list ?A) (x : ?A),
f <$> l = f' <$> l → x ∈ l → f x = f' x