proposition: Lemma eq_bool_ok : forall al1 al2, match eq_bool al1 al2 with true => al1 = al2 | false => ~al1 = al2 end.
proof: Proof. intros [e1 l1] [e2 l2]; simpl. generalize (DS1.eq_bool_ok e1 e2); case (DS1.eq_bool e1 e2); [intros e1_eq_e2 | intros e1_diff_e2]. revert l1 l2. assert (H : forall l1 l2, match eq_bool_list l1 l2 with true => l1 = l2 | false => ~l1 = l2 end). fix eq_bool_ok0 1. intros [ | a1 l1] [ | a2 l2]; simpl. apply eq_refl. discriminate. discriminate. generalize (DS1.eq_bool_ok a1 a2); case (DS1.eq_bool a1 a2); [intros a1_eq_a2 | intros a1_diff_a2]. generalize (eq_bool_ok0 l1 l2); case (eq_bool_list l1 l2); [intro l1_eq_l2 | intro l1_diff_l2]. subst; apply eq_refl. intro E; apply l1_diff_l2; injection E; intros; subst; apply eq_refl. intro E; apply a1_diff_a2; injection E; intros; subst; apply eq_refl. intros l1 l2; generalize (H l1 l2). case (eq_bool_list l1 l2); [intro l1_eq_l2 | intro l1_diff_l2]. subst; apply (equiv_refl _ _ eq_proof). intro E; apply l1_diff_l2; injection E; intros; subst; apply eq_refl. intro E; apply e1_diff_e2; injection E; intros; subst; apply eq_refl. Defined.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)