proposition: Lemma well_formed_RndNat : forall n, n > O -> well_formed_comp (RndNat n).
proof: Proof. intuition. unfold RndNat. eapply (well_formed_Repeat). unfold eq_dec. intuition idtac. eapply eq_nat_dec. unfold RndNat_unchecked. eapply well_formed_Bind. eapply well_formed_Rnd. intuition. eapply well_formed_Ret. eapply filter_In. intuition. 2:{ unfold ltNatBool. assert ((if (lt_dec O n) then true else false) = true). destruct (lt_dec O n). trivial. lia. eapply H0. } simpl. eapply Fold.in_getUnique. eapply Fold.in_flatten. econstructor. split. eapply in_map_iff. econstructor. split. eauto. eapply in_getAllBvectors. specialize (bvNat_zero (lognat n)); intuition. simpl in *. left. eapply H0. Qed.
imports: FCF.Crypto Permutation FCF.NotationV1