proposition: Lemma lForallSame: forall {A : Type} (P : A -> [univ]) (l : list A), lForall P l <=> lforall P l.
proof: Proof. induction l; allsimpl; unfold lforall; repnd; split; cpx; introv Hyp; repnd. - apply IHl in Hyp. introv Hin. allsimpl. dorn Hin; subst; cpx. - dands; cpx. apply IHl. introv Hin. apply Hyp. right; cpx. Qed.
imports: UsefulTypes bin_rels Omega