proposition: Lemma eval_det : forall ectx t v v', TmEval ectx t v -> TmEval ectx t v' -> v = v'.
proof: Proof. intros t ectx v v' H; revert v'; induction H; intros v2 H'; inversion H'; subst; auto; try congruence. assert (v = v0) by firstorder. subst v. assert (H2 : VAbs t' ectx' = VAbs t'0 ectx'0) by firstorder. inversion H2; subst. now auto. Defined.
imports: List Arith Bool