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