proposition: Lemma qf_evalE (e : seq R) (f : formula R) : qf_eval e f = ord.qf_eval e f.
proof: Proof. by elim: f=> /=; do ?[rewrite evalE|move->|move=> ?]. 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)