proposition: Lemma lforall_incl l1 l2 : l1 [= l2 -> lforall l2 -> lforall l1.
proof: Proof. intros. apply lforall_intro. intros. eapply lforall_in. apply H0. apply H. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)