proposition: Lemma eval_tsubst e t s : eval e (tsubst t s) = eval (set_nth 0 e s.1 (eval e s.2)) t.
proof: Proof. case: s => i u; elim: t => //=; do 2?[move=> ? -> //] => j. by rewrite nth_set_nth /=; case: (_ == _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)