proposition: Theorem getUnusedBvector_wf : forall ls d, well_formed_Bvector_perm ls -> ls # d = None -> well_formed_comp (getUnusedBvector ls).
proof: Proof. intuition. eapply well_formed_perm_1 in H. destruct H. intuition. unfold getUnusedBvector. eapply getUnusedR_wf; wftac. eauto. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF