proposition: Lemma rev_incl : forall l : list A, rev l [= l.
proof: Proof. intros. pose (incl_rev (rev l)). rewrite (rev_involutive l) in i. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)