simp [Tensor1D.fill, Tensor1D.extract]
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ Tensor1D.fill (Tensor1D.extract t extractlen) fillval = Tensor1D.extract (Tensor1D.fill t fillval) extractlen
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.replicate (min extractlen t.size0) fillval = List.take extractlen (List.replicate t.size0 fillval)