handle let expressions inside terms by unfolding (instead of raising an exception),
added examples to test this feature
#2 := false
#8 := 1::real
decl uf_1 :: real
#4 := uf_1
#6 := 2::real
#7 := (* 2::real uf_1)
#9 := (+ #7 1::real)
#5 := (+ uf_1 uf_1)
#10 := (< #5 #9)
#11 := (or false #10)
#12 := (or #10 #11)
#13 := (not #12)
#64 := (iff #13 false)
#32 := (+ 1::real #7)
#35 := (< #7 #32)
#52 := (not #35)
#62 := (iff #52 false)
#1 := true
#57 := (not true)
#60 := (iff #57 false)
#61 := [rewrite]: #60
#58 := (iff #52 #57)
#55 := (iff #35 true)
#56 := [rewrite]: #55
#59 := [monotonicity #56]: #58
#63 := [trans #59 #61]: #62
#53 := (iff #13 #52)
#50 := (iff #12 #35)
#45 := (or #35 #35)
#48 := (iff #45 #35)
#49 := [rewrite]: #48
#46 := (iff #12 #45)
#43 := (iff #11 #35)
#38 := (or false #35)
#41 := (iff #38 #35)
#42 := [rewrite]: #41
#39 := (iff #11 #38)
#36 := (iff #10 #35)
#33 := (= #9 #32)
#34 := [rewrite]: #33
#30 := (= #5 #7)
#31 := [rewrite]: #30
#37 := [monotonicity #31 #34]: #36
#40 := [monotonicity #37]: #39
#44 := [trans #40 #42]: #43
#47 := [monotonicity #37 #44]: #46
#51 := [trans #47 #49]: #50
#54 := [monotonicity #51]: #53
#65 := [trans #54 #63]: #64
#29 := [asserted]: #13
[mp #29 #65]: false
unsat