proposition: Lemma well_formed_perm_cons : forall ls d r, well_formed_perm ls -> ls#d = None -> inRange ls r = false -> well_formed_perm ((d, r) :: ls).
proof: Proof. unfold well_formed_perm in *. intuition. destruct (in_dec (EqDec_dec _) d lsd). specialize (H3 d). intuition. simpl in *. rewrite eqb_refl in H4. discriminate. edestruct (H (d :: lsd)). econstructor; trivial. intuition. simpl in *. intuition. subst. trivial. specialize (H3 d0). intuition. destruct (eqb d0 d). discriminate. trivial. intuition. destruct (in_dec (EqDec_dec _) r x). exists (removeFirst (EqDec_dec _) x r). intuition. simpl. case_eq (eqb r0 r); intuition. rewrite eqb_leibniz in H8. subst. exfalso. eapply removeFirst_NoDup_not_in. eapply H4. eapply H6. eapply H5. eapply removeFirst_in_iff. eauto. eapply H5. eapply removeFirst_in_iff. eauto. eapply removeFirst_NoDup. trivial. simpl in H7. eapply eq_add_S. rewrite H7. symmetry. eapply removeFirst_length. trivial. destruct x. simpl in *. lia. exists x. intuition. simpl in *. intuition. case_eq (eqb r1 r); intuition. exfalso. rewrite eqb_leibniz in H10. subst. intuition. eapply H5. right. trivial. eapply H5. simpl. intuition. inversion H4; clear H4; subst. trivial. Qed.
imports: Crypto Permutation CompFold Array FCF State