proposition: Lemma lforall_imp A (P1 P2 : A->Prop) : (forall x, P1 x -> P2 x) -> forall l, lforall P1 l -> lforall P2 l.
proof: Proof. intros H l. elim l. intuition. intros a' l' Hrec. simpl. intros (H1, H2). split. apply H. hyp. apply Hrec. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)