proposition: Lemma incl_flat_In : forall x c cs l, In x c -> In c cs -> flat cs [= l -> In x l.
proof: Proof. intros. apply H1. apply (In_incl_flat _ _ H0). hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)