List fold/map with membership evidence

Stream: Is there code for X?

[Valentin Robert]

I have not found something like these:

def foldWithMembership (l : List α) (init : β) (f : (x : α) → x ∈ l → β → β) : β :=
  match l with
  | [] => init
  | x :: xs =>
    f x List.mem_cons_self
      (foldWithMembership xs init (fun y xl b => f y (List.mem_cons_of_mem x xl) b))

def mapOnWithMembership (l : List α) (f : (x : α) → x ∈ l → β) : List β :=
    foldWithMembership l [] (fun x xmem tl => f x xmem :: tl)

Do they exist somewhere? In fact I'm surprised people can handle nested recursive datatypes containing lists without these, how do they prove termination when they map a recursive call over a list if they don't get evidence that the elements in the list belonged in the list?

[Eric Wieser]

docs#List.attach

[Eric Wieser]

And perhaps docs#List.pmap