proposition: Lemma In_incl_flat : forall x l, In x l -> x [= flat l.
proof: Proof. induction l; simpl; intros. contr. intuition. subst. apply incl_appl. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)