proposition: Lemma eq_sat f1 f2 : (forall e, holds e f1 <-> holds e f2) -> sat^~ f1 =1 sat^~ f2.
proof: Proof. by move=> eqf12 e; apply/satP/satP; case: (eqf12 e). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)