proposition: Theorem last_snoc: forall A (l:list A) (a d:A) , nth (length l) (snoc l a) d= a.
proof: Proof. induction l ; introv . refl. rewrite snoc_as_append. rewrite app_nth2. simpl. asserts_rewrite (length l - length l=0); try omega. auto. omega. Qed.
imports: UsefulTypes bin_rels Omega