proposition: Lemma eval_If e pf tf ef (ev := qf_eval e) : ev (If pf Then tf Else ef) = (if ev pf then ev tf else ev ef).
proof: Proof. by unlock (If _ Then _ Else _)=> /=; case: ifP => _; rewrite ?orbF. 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)