Updated snapshot injectivity axiom.

[zgrannan]

The snapshot domain axioms do not currently ensure that a snapshot for a variant must correspond to a constructor invocation. As a consequence, given snapshots s1 and s2 that return the same values for all field access functions, we cannot prove s1 == s2 (see the included test).

This PR introduces a new injectivity axiom, asserting that each variant snapshot corresponds to a constructor invocation:

forall this: Variant :: 
  {field1(this), field2(this), ...}
  this == cons(field1(this), field2(this), ...)

The replaces the current injectivity axiom:

forall _l_args..., _r_args... :: {cons(_l_args...), cons(_r_args)}
    cons(_l_args...) == cons(_r_args) ==> _l_args... == _r_args...

The trigger on field access axioms is also made more permissive. This is necessary because the new injectivity axiom is only triggered on field access (and not on snapshot construction).

Previous: forall args... :: {field(cons(arg_field, other_args...))} field(cons(arg_field, other_args...)) == arg_field
New: forall args... :: {cons(arg_field, other_args...)} field(cons(arg_field, other_args...)) == arg_field

Finally, DefinitionCollector is updated to ensure that functions used in the triggers of domain axioms are always preserved.