proposition: Lemma eq_sol f1 f2 : (forall e, holds e f1 <-> holds e f2) -> sol^~ f1 =1 sol^~ f2.
proof: Proof. rewrite /sol => /eq_sat eqf12 n. do 2![case: sol_subproof] => //= [f1s f2s | ns1 [s f2s] | [s f1s] []]. - by apply: eq_xchoose => s; rewrite eqf12. - by case: ns1; exists s; rewrite -eqf12. by exists s; rewrite eqf12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)