can't go further than that ...
added list + inductive patch
finally got it right
new patch
new patch works ... but provers are still dumb