proposition: Lemma eval_Changes e s k : qf_eval e (Changes s k) = qf_eval e (k (changes (map (eval e) s))).
proof: Proof. elim: s k=> //= a q ihq k; rewrite ihq eval_If /= -nth0. by case: q {ihq}=> /= [|b q]; [rewrite /= mulr0 ltxx add0n | case: ltrP]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)