proposition: Lemma rev_list_ind : forall (A : Type) (P : list A -> Prop), P [] -> (forall (a : A) (l : list A), P l -> P (snoc l a)) -> forall l : list A, P l.
proof: Proof. intros. assert ({n : nat $ length l = n}) as p by (exists (length l); auto). destruct p as [n e]. revert l e. induction n; intros. apply length0 in e; subst; sp. generalize (snoc_cases A l); sp; subst; auto. apply H0. apply IHn. allrewrite length_snoc; allapply S_inj; auto. Qed.
imports: UsefulTypes bin_rels Omega