proposition: Theorem wf_triple : well_founded eval_rel.
proof: Proof. intros [ectx t [v red_v]]. constructor. intros [ectx_y t_y [v_y red_v_y]]; unfold eval_rel; simpl. intros; eapply Acc_lemma; [ | reflexivity]. simpl. eapply acc_tmeval; eauto. Defined.
imports: List Arith Bool Wellfounded