proposition: Lemma lforall_in a l : lforall l -> In a l -> P a.
proof: Proof. elim l. intros H1 H2. absurd (In a nil); [apply in_nil | hyp]. intros b l' Hrec H1 H2. elim (in_inv H2). intro H3. subst a. unfold lforall in H1. intuition. clear H2. intro H2. gen (lforall_cons H1). intros (H3, H4). apply (Hrec H4 H2). Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)