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

Ah, good catch... should we change that default at least for some sections of that file, or will that not work?

added 1 commit

• 4bbaa43a - Fix list_fmap_inj_1

Compare with previous version

resolved all threads

merged

mentioned in commit c531cb8b