sorry
case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
no goals