proposition: Lemma incl_nil_elim : forall l : list A, l [= nil <-> l = nil.
proof: Proof. unfold incl. destruct l; intuition. assert (In a (a::l)). left. refl. ded (H _ H0). contr. discr. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)