Convert many examples to java backend

**do not review yet**
see above. This relates to polymorphic-identity-2-fails. The problem is that the smtlib does not know that it can not unify T1 -> T2 = T1, and so it adds this as a constraint and continues to rewrite, and so eventually, instead of getting stuck, it outputs that the type of the program is a variable, and does not realize that the constraint is not actually satisfied.