## Stream: general

### Topic: simp list.map id

#### Sean Leather (Sep 28 2018 at 08:58):

Interesting that simp doesn't solve list.map (λ t, t) l = l.

#### Sean Leather (Sep 28 2018 at 08:59):

I suppose I could add this to the simp:

 theorem map_id' {f : α → α} (h : ∀ x, f x = x) (l : list α) : map f l = l


#### Sean Leather (Sep 28 2018 at 09:00):

Yep, simp [list.map_id'] does the job.

Last updated: May 11 2021 at 00:31 UTC