证明了 expr_type_map_sound

改进了 eeval_coincide 在 EConst i t ts 的证明

之前的证明没有直接处理 rew type_map_sound ... in eeval (EConst i t ts)，而是把这部分证明“外包”给 const_asgn_coincide_on 来证。现在直接证明了两个 rew 等价。

Universe Inconsistency

Universe Inconsistency error when proving eeval_coincide

Cannot enforce u1 = u2 be u1 < u2

Adding Polymorphic to some lemmas rew_none, rew_some solves the issue. But I don't know why.

Polymorphic Lemma rew_some {A B} (H: A = B) (x: A) :
  rew [fun T => option T] H in Some x = Some (rew H in x).
Proof. subst. reflexivity. Qed.

Polymorphic Lemma rew_none {A B} (H: A = B) :
  rew [fun T => option T] H in None = None.
Proof. subst. reflexivity. Qed.

A Previous Issue and Its Solution

Replace rew [option] eq in x with rew [fun T => option T] eq in x to relax the universe constraint.

This is because eeval uses option, so eeval.u < option.u is required. rew [fun T: Type@{u} => option T] eq in eeval ... only requires u < option.u and u < eeval.u. But rew [option] eq in eeval ... requires option.u = x.u, which is not true.