proposition: Lemma Fnorm_bf_correct k (ff : BFormula (RFormula F) k) : eval_bf Feval_formula ff = eval_bf Fnorm_formula ff.
proof: Proof. elim: ff => // {k}. - by move=> k ff ?; exact: Fnorm_formula_correct. - by move=> k ff1 IH1 ff2 IH2; congr eAND. - by move=> k ff1 IH1 ff2 IH2; congr eOR. - by move=> k ff IH; congr eNOT. - by move=> k ff1 IH1 o ff2 IH2; congr eIMPL. - by move=> k ff1 IH1 ff2 IH2; congr eIFF. - by move=> ff1 IH1 ff2 IH2; congr eq. Qed.
imports: elpi(elpi) Coq(QArith Ring) Coq.micromega(RingMicromega QMicromega EnvRing Tauto Lqa) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)