prove general fmap_inj lemmas
Compare changes
+ 31
− 16
@@ -504,6 +504,13 @@ Lemma list_singleton_reflect l :
@@ -3686,21 +3693,21 @@ Section setoid.
@@ -3744,13 +3751,13 @@ Section setoid.
@@ -3773,7 +3780,7 @@ Section setoid.
@@ -3946,12 +3953,6 @@ Section fmap.
@@ -4059,6 +4060,20 @@ Section fmap.