tests/theorem-rand.scm is beautiful!
e.g.
theorem vec-zip ∀ v ∊ (Vector-of Short) (vector-zip + v v) = (vector-map (λ (x) (* x 2)) v)