proposition: Lemma in_rev : forall (x : A) l, In x l -> In x (rev l).
proof: Proof. induction l; simpl; intros. hyp. apply in_or_app. simpl. tauto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)