proposition: Lemma inj_pos x y : forall l, In x l -> pos x l = pos y l -> x = y.
proof: Proof. induction l; intro h; simpl. contr. destruct (eq_dec a x); destruct (eq_dec a y); subst; intro e. reflexivity. discr. discr. inversion e. fo. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)