better intensional set and enum set

[malloc-realloc]

Set the symbol with a value

claim: forall s, s2 set: s := {x R: 1 <= x < 10, x %2 = 0} s2 := {2, 4, 6, 8} =>: s = s2 # 根据 s >= s2, s <= s2，所以 s = s2 prove: prove_by_enum(x s2): x $in s # 如果s是intensional set，那我会自动帮你 prove_by_set_def一下 prove_in_range(1, 10, x s): # 先验证 s 里面的元素真的满足 1 <= x < 10，然后对于那些满足条件的x进行遍历证明 x %2 = 0 x $in s2 # 如果s2是枚举型集合，那我会一个个比较你是不是真的等于 s2 里面的元素

更新：

1. = { 而不是 := 作为set的定义，以后这个 = 会和 := 等价 这是对parse的更新 1.1 = {

2. inline intensional

:= 更强大一点: 还能做赋值

4. prove_by_enum 而不是 prove_over_finite_set

5. 更强大的 prove_in_range，能读入一个集合，这个集合是range的子集