proposition: Lemma beq_list_ok_in : forall l, forall hyp : forall x, In x l -> forall y, beq x y = true <-> x = y, forall m, beq_list l m = true <-> l = m.
proof: Proof. induction l; destruct m; split; intro; try (refl || discr). inversion H. destruct (andb_elim H1). assert (h : In a (a::l)). simpl. auto. ded (hyp _ h a0). rewrite H3 in H0. subst a0. apply tail_eq. assert (hyp' : forall x, In x l -> forall y, beq x y = true <-> x=y). intros x hx. apply hyp. simpl. auto. destruct (andb_elim H1). ded (IHl hyp' m). rewrite H5 in H4. exact H4. rewrite <- H. simpl. apply andb_intro. assert (h : In a (a::l)). simpl. auto. ded (hyp _ h a). rewrite H0. refl. assert (hyp' : forall x, In x l -> forall y, beq x y = true <-> x=y). intros x hx. apply hyp. simpl. auto. ded (IHl hyp' l). rewrite H0. refl. Qed.
imports: Coq(Arith Lia) CoLoR(ListUtil BoolUtil EqUtil LogicUtil)