Field and predicate specific FVFs

[marcoeilers]

Making FVF sorts (and the predicate equivalent) field-specific. The point is to avoid triggering the FVF extensionality axioms on pairs of FVFs of different fields (or predicates), which is never useful, and looks potentially expensive.

Draft, still testing performance implications.

[jcp19]

@marcoeilers does this lead to any noticeable speed-up in our benchmarks?

PS: I can also test it on SCION if you need more benchmarking data

[jcp19]

Did a few extra tests with SCION packages. In one instance (package slayers/path/onehop) this lead to a drop in half of the verification time (from 6min16s to 3min36s). For the router package, verification went from ~30min to ~26min