
  0 | module Libraries.Data.List.HasLength
  1 | 
  2 | import Data.Nat
  3 | 
  4 | import Data.List.HasLength
  5 | 
  6 | export
  7 | cast : {ys : _} -> (0 _ : List.length xs = List.length ys) -> HasLength m xs -> HasLength m ys
  8 | cast {ys = []}      eq Z = Z
  9 | cast {ys = y :: ys} eq (S p) = S (cast (injective eq) p)
 10 |