Error "not termf" from quickcheck

[brianhuffman]

First, define a polymorphic cryptol predicate like this:

foo : {n} (fin n) => [n] -> Bit
foo x = x == x

Then load it in saw and try to prove a type instance of it using quickcheck:

sawscript> import "test.cry"
sawscript> prove (quickcheck 100) {{ foo`{8} }}
[04:11:55.775] WARNING: using quickcheck to prove goal...

user error ("prove" (<stdin>:1:1-1:6):
"quickcheck" (<stdin>:1:8-1:18):
not ftermf)