proposition: Lemma well_formed_perm_1 : forall ls, well_formed_perm ls -> forall d, ls#d = None -> exists r, inRange ls r = false /\ In r (getSupport RndR).
proof: Proof. intuition. specialize (H (d :: nil)). edestruct H. econstructor. simpl. intuition. econstructor. intuition. simpl in *. intuition. subst. trivial. intuition. destruct x. simpl in *. lia. destruct x; simpl in *. econstructor. eapply H2. intuition. lia. Qed.
imports: Crypto Permutation CompFold Array FCF State