apply List.extF
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.replicate (min extractlen t.size0) fillval = List.take extractlen (List.replicate t.size0 fillval)
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ ∀ (n : ℕ) (h : n < List.length (List.replicate (min extractlen t.size0) fillval)),
    List.getF (List.replicate (min extractlen t.size0) fillval) n h =
      List.getF (List.take extractlen (List.replicate t.size0 fillval)) n
        (_ : n < List.length (List.take extractlen (List.replicate t.size0 fillval)))

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))