proposition: Lemma null_iff_nil : forall T, forall l : list T, null l <=> l = [].
proof: Proof. induction l; unfold null; simpl; split; sp. assert ((a = a) [+] LIn a l) by (left; auto). apply_in_hyp p; sp. Qed.
imports: UsefulTypes bin_rels Omega