fact: Fixpoint BFormula_Q2Z [k] (ff : BFormula (Formula Q) k) : option (BFormula (Formula Z) k) := match ff with | TT k => Some (TT k) | FF k => Some (FF k) | X k P => Some (X k P) | A k a aa => omap (A k ^~ aa) (Formula_Q2Z a) | AND _ f1 f2 => omap2 (fun f => AND f) (BFormula_Q2Z f1) (BFormula_Q2Z f2) | OR _ f1 f2 => omap2 (fun f => OR f) (BFormula_Q2Z f1) (BFormula_Q2Z f2) | NOT _ f1 => omap (fun f => NOT f) (BFormula_Q2Z f1) | IMPL _ f1 o f2 => omap2 (fun f => IMPL f o) (BFormula_Q2Z f1) (BFormula_Q2Z f2) | IFF _ f1 f2 => omap2 (fun f => IFF f) (BFormula_Q2Z f1) (BFormula_Q2Z f2) | EQ f1 f2 => omap2 EQ (BFormula_Q2Z f1) (BFormula_Q2Z f2) end.
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)