Evaluation anf inference of formulas are now hconsed (in Formula).