proposition: Lemma permut_bool_ok : forall l1 l2, match permut_bool l1 l2 with true => permut l1 l2 | false => ~permut l1 l2 end.
proof: Proof. fix permut_bool_ok 1. intro l1; case l1; clear l1. intro l2; case l2; clear l2. simpl; apply Pnil. intros a2 l2 P; inversion P. intros a1 l1 l2; simpl. generalize (in_remove _ _ EDS1.eq_bool_ok a1 l2); case (remove eq_bool a1 l2). intros k2 [a2 [l2' [l2'' [a1_eq_a2 [H H']]]]]; injection H'; clear H'; intro H'. generalize (permut_bool_ok l1 k2); case (permut_bool l1 k2). intro P; subst; apply Pcons; assumption. intros not_P P'; apply not_P. subst k2; rewrite (permut_cons_inside l1 l2' l2'' a1_eq_a2); subst l2; apply P'. intros a1_diff_a2 P; apply a1_diff_a2. rewrite <- (mem_permut_mem a1 P); left. reflexivity. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)