proposition: Theorem acc_tmeval : forall e t v, TmEval e t v -> Acc TmEvalRel (e, t).
proof: Proof. intros e t v h; induction h; constructor; intros [e1 t1] lt_t_t1; inversion lt_t_t1; subst; try congruence. assert (v = v0) by eauto; subst. assert (h : VAbs t' ectx' = VAbs t1 e') by eauto. inversion h; subst. auto. Defined.
imports: List Arith Bool