1 (1) Elements/BooleanVars should link back to expressions that use them
3 (2) Need to introduce variables in encoding of functions....
5 (3) Some cases can do variable elimination of introduced variables...
7 (4) Might need to indicate what variables we can query about in
10 (5) Could simplify output of functions... Maybe several outputs have