proposition: Lemma Inb_equiv : forall x l l', lequiv l l' -> Inb x l = Inb x l'.
proof: Proof. intros. destruct H. case_eq (Inb x l'); intros; case_eq (Inb x l); intros; try refl. ded (Inb_incl _ H0 H1). rewrite H2 in H3. discr. ded (Inb_incl _ H H2). rewrite H1 in H3. discr. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)