在 cicada 中，用最简单的 dependent type Exp 实验 type check by propagator 还是需要 Exp Value Neutral，但是不用 Core [maybe] 保留 check 和 infer 这些函数的 interface，但是用 propagator 实现？ 语法 -- 回到数学的语法 f(x)，不一定要模仿 JS。