proposition: Lemma eval_nth_rcons_unique : forall d vars vars' e l, eval e vars = eval e vars' -> (forall n, eval (nth n l d) vars = eval (nth n l d) vars') -> forall n, eval (nth n (rcons_unique e l) d) vars = eval (nth n (rcons_unique e l) d) vars'.
proof: Proof. intros d vars vars' e l He Hl. induction l as [|h t IH] ; simpl. { simpl in Hl. now intros [|n]. } generalize (internal_expr_dec_bl e h). destruct expr_beq. { now intros _. } intros _ [|n]. { apply (Hl 0). } apply IH. intros n'. apply (Hl (S n')). Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree