proposition: Lemma eq_holds e e' f : same_env e e' -> holds e f -> holds e' f.
proof: Proof. pose sv := set_nth (0 : R). have eq_i i v e1 e2: same_env e1 e2 -> same_env (sv e1 i v) (sv e2 i v). by move=> eq_e j; rewrite !nth_set_nth /= eq_e. elim: f e e' => //=. - by move=> t1 t2 e e' eq_e; rewrite !(eq_eval _ eq_e). - by move=> t e e' eq_e; rewrite (eq_eval _ eq_e). - by move=> f1 IH1 f2 IH2 e e' eq_e; move/IH2: (eq_e); move/IH1: eq_e; tauto. - by move=> f1 IH1 f2 IH2 e e' eq_e; move/IH2: (eq_e); move/IH1: eq_e; tauto. - by move=> f1 IH1 f2 IH2 e e' eq_e f12; move/IH1: (same_env_sym eq_e); eauto. - by move=> f1 IH1 e e'; move/same_env_sym; move/IH1; tauto. - by move=> i f1 IH1 e e'; move/(eq_i i)=> eq_e [x f_ex]; exists x; eauto. by move=> i f1 IH1 e e'; move/(eq_i i); eauto. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)