proposition: Fact sol_subproof n f : reflect (exists s, (size s == n) && sat s f) (sat [::] (foldr Exists f (iota 0 n))).
proof: Proof. apply: (iffP (satP _ _)) => [|[s]]; last first. case/andP=> /eqP sz_s /satP f_s; apply/foldExistsP. exists s => // i; rewrite !inE mem_iota -leqNgt add0n => le_n_i. by rewrite !nth_default ?sz_s. case/foldExistsP=> e e0 f_e; set s := take n (set_nth 0 e n 0). have sz_s: size s = n by rewrite size_take size_set_nth leq_max leqnn. exists s; rewrite sz_s eqxx; apply/satP; apply: eq_holds f_e => i. case: (leqP n i) => [le_n_i | lt_i_n]. by rewrite -e0 ?nth_default ?sz_s // !inE mem_iota -leqNgt. by rewrite nth_take // nth_set_nth /= eq_sym eqn_leq leqNgt lt_i_n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)