Skip to content

Fix list_fmap_inj_1

Michael Sammler requested to merge msammler/fix_list_fmap_inj_1 into master

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

Merge request reports

Loading