proposition: Lemma lforallApp: forall {A : Type} (P : A -> [univ]) (la lb : list A), lforall P (la ++ lb) <=> lforall P la # lforall P lb.
proof: Proof. intros. split; introv Hyp; dands; repnd; try introv Hin; allrw in_app_iff; cpx; apply Hyp; apply in_app_iff; cpx. Qed.
imports: UsefulTypes bin_rels Omega