proposition: Lemma eval_var a z: eval (s a) (t a) (e_var a) z -> z=e_var a.
proof: Proof. assert (G: forall n m u (z: expr n m), eval n m u z -> forall a (Hs: s a=n) (Ht: t a=m), u=e_var a -> z = eq_rect _ (fun m => expr m _) (eq_rect _ (expr _) (e_var a) m Ht) n Hs). intros n m u z'. destruct 1; intros b Hs Ht E; try discriminate. injection E. intros ->. now rewrite 2cmp_eq_rect_eq. intro Hz. apply (G _ _ _ _ Hz _ eq_refl eq_refl eq_refl). Qed.
imports: kleene syntax