Fix list_fmap_inj_1
All threads resolved!
All threads resolved!
Compare changes
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 xThis 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