proposition: Lemma lforall_dec : forall l, {lforall l} + {~lforall l}.
proof: Proof. induction l. left. simpl. trivial. simpl. destruct (@P_dec a). destruct IHl. left; auto. right; intuition. right; intuition. Defined.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)