Repeat returns a list of Cons's

We can prove that `repeat` returns a `List` with no `Nil`s, and that we can safely `take` any number of elements from `repeat`.

The code is somewhat hacky, I've changed `refresh` to only expand `Ref`s twice so we don't get an infinite loop when trying to expand a recursive `Ref`. This required changing a few `safeZip`s in `Constraint` to regular `zip`s because not all instances of an `RApp` will have the correct number of `Ref`s.. But it works empirically, i.e. none of our existing tests break..