proposition: Lemma eq_eval e e' t : same_env e e' -> eval e t = eval e' t.
proof: Proof. by move=> eq_e; elim: t => //= t1 -> // t2 ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)