proposition: Lemma holds_fsubst e f i v : holds e (fsubst f (i, v%:T)%T) <-> holds (set_nth 0 e i v) f.
proof: Proof. elim: f e => //=; do [ by move=> *; rewrite !eval_tsubst | move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto | move=> f IHf e; move: (IHf e); tauto | move=> j f IHf e]. - case eq_ji: (j == i); first rewrite (eqP eq_ji). by split=> [] [x f_x]; exists x; rewrite set_set_nth eqxx in f_x *. split=> [] [x f_x]; exists x; move: f_x; rewrite set_set_nth eq_sym eq_ji; have:= IHf (set_nth 0 e j x); tauto. case eq_ji: (j == i); first rewrite (eqP eq_ji). by split=> [] f_ x; move: (f_ x); rewrite set_set_nth eqxx. split=> [] f_ x; move: (IHf (set_nth 0 e j x)) (f_ x); by rewrite set_set_nth eq_sym eq_ji; tauto. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)