Where then we say and

Thus we have for

Similarly, for we have and

Thus for we have

TODO

  • Fix typos in Readme
  • Add global vartype to readme
  • make pr of global vartype
  • fix inequality encoding
  • add some documentation how the encoding works (i.e. linearisation)
  • check if I mutate the ast in parse model
  • check that the order of operations is correct for linearisation
  • I don't believe it works with equality (I think I know how to add it though)