proposition: Lemma lforall_app l2 : forall l1 : list A, lforall (l1 ++ l2) <-> lforall l1 /\ lforall l2.
proof: Proof. induction l1; simpl; intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)