proposition: Lemma qf_evalP e f : qf_form f -> reflect (holds e f) (qf_eval e f).
proof: Proof. elim: f => //=; try by move=> *; apply: idP. - by move=> t1 t2 _; apply: eqP. - move=> f1 IHf1 f2 IHf2 /= /andP[/IHf1[] f1T]; last by right; case. by case/IHf2; [left | right; case]. - move=> f1 IHf1 f2 IHf2 /= /andP[/IHf1[] f1F]; first by do 2 left. by case/IHf2; [left; right | right; case]. - move=> f1 IHf1 f2 IHf2 /= /andP[/IHf1[] f1T]; last by left. by case/IHf2; [left | right; move/(_ f1T)]. by move=> f1 IHf1 /IHf1[]; [right | left]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)