Try these:
  [apply] [grind =] for pattern: [@List.length #2 (@List.cons _ #1 #0)]
  [apply] [grind! .] for pattern: [@List.cons #2 #1 #0]
Try these:
  [apply] [grind =] for pattern: [@List.length #0 (@List.nil _)]
  [apply] [grind! .] for pattern: [@List.nil #0]
Try these:
  [apply] [grind =] for pattern: [@getElem (List #4) `[Nat] _ _ _ (@List.cons _ #2 #1) #3 #0]
  [apply] [grind →] for pattern: [@LE.le `[Nat] `[instLENat] (#3 + 1) (@List.length #4 (@List.cons _ #2 #1))]
Try this:
  [apply] [grind =] for pattern: [@getElem? (List #3) `[Nat] _ _ _ (@List.cons _ #2 #1) #0]
Try this:
  [apply] [grind =] for pattern: [@getElem? (List #1) `[Nat] _ _ _ (@List.nil _) #0]