proposition: Lemma well_formed_perm_cons_2 : forall ls d r1 r2, well_formed_perm ls -> inRange ls r2 = true -> ls#d = None -> well_formed_perm ((d, r1) :: (d, r2) :: ls).
proof: Proof. intuition. unfold well_formed_perm. 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 H4. intuition. subst. trivial. specialize (H3 d0). intuition. simpl in *. destruct (eqb d0 d). discriminate. trivial. intuition. destruct (in_dec (EqDec_dec _) r1 x). exists (removeFirst (EqDec_dec _) x r1). intuition. simpl. case_eq (eqb r r1); intuition. rewrite eqb_leibniz in H8. subst. exfalso. eapply removeFirst_NoDup_not_in. eapply H4. eauto. case_eq (eqb r r2); intuition. rewrite eqb_leibniz in H9. subst. assert (inRange ls r2 = false). eapply H5. eapply removeFirst_in_iff. eauto. congruence. eapply H5. eapply removeFirst_in_iff. eauto. eapply H5. eapply removeFirst_in_iff. eauto. eauto using removeFirst_NoDup. eapply eq_add_S. simpl in H7. rewrite H7. symmetry. eapply removeFirst_length. trivial. destruct x. simpl in *. lia. exists x. intuition. simpl in *. case_eq (eqb r0 r1); intuition. rewrite eqb_leibniz in H8. subst. intuition. case_eq (eqb r0 r2); intuition. rewrite eqb_leibniz in H11. subst. assert (inRange ls r2 = false). eapply H5. intuition. congruence. eapply H5. intuition. eapply H5. simpl. intuition. inversion H4; clear H4; subst. trivial. Qed.
imports: Crypto Permutation CompFold Array FCF State