proposition: Lemma eval_dot n m x y z: eval n m (x⋅y) z -> exists p, exists x', eval n p x x' /\ exists y', eval p m y y' /\ z=e_dot x' y'.
proof: Proof. remember (x⋅y)%ast as z' eqn:E. destruct 1; try discriminate. generalize (f_equal ((fun n m e => match e in syntax.expr _ _ n m return syntax.expr _ _ n xH with | @e_dot _ _ _ _ p _ x _ => match eqb_spec cmp_pos p xH with | reflect_t H => eq_rect _ (syntax.expr _ _ _) x _ H | _ => e_zer _ _ end | _ => e_zer _ _ end) xH xH) E). case eqb_spec. 2: congruence. intro. rewrite 2cmp_eq_rect_eq. intros <-. generalize (f_equal ((fun n m e => match e in syntax.expr _ _ n m return syntax.expr _ _ xH m with | @e_dot _ _ _ _ p _ _ x => match eqb_spec cmp_pos p xH with | reflect_t H => eq_rect _ (fun p => syntax.expr _ _ p _) x _ H | _ => e_zer _ _ end | _ => e_zer _ _ end) xH xH) E). case eqb_spec. 2: congruence. intro. rewrite 2cmp_eq_rect_eq. intros <-. eauto 6. Qed.
imports: kleene syntax