renaming `List.foldr_self_append`

Stream: Is there code for X?

[Kim Morrison]

Any suggestions for a better name for:

List.foldr_self_append.{u_1} {α : Type u_1} {l' : List α} (l : List α) : foldr cons l' l = l ++ l'

?

Of course List.foldr_cons is already taken. :-)

[Kim Morrison]

There will also be theorem foldl_flip_cons (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l', which I don't mind renaming for consonance.

[Daniel Weber]

Perhaps List.foldr_cons_eq_append?

[Eric Wieser]

Or some more symbol reading, as foldr_cons_left