配列(リスト)の逆順に関する性質の証明

https://gist.github.com/4243787

最近、プログラマの採用面接で解かす問題集みたいな本が出て
その中に「ある配列がユニークであるかどうかを示すコードを書け」という問いがあり、Coqで書いてみました。
下記のようなコードになるんだけどついでに配列を逆にした場合も結果は同じであろうという直感を証明しようと思ったらすごく嵌りました。

Require Import Bool.
Require Import Lists.List.
Require Import String.
Require Import Ascii.

Definition eqc (x y : ascii) : bool :=
  if ascii_dec x y
    then true
    else false.

Fixpoint list_of_string (s : string) : list ascii :=
  match s with
  | EmptyString => nil
  | String c s => c :: (list_of_string s)
  end.

Fixpoint contain (c : ascii) (chars : list ascii) : bool :=
  match chars with
    | nil => false
    | x :: xs =>
      if eqc x c then
        true
      else
        contain c xs
  end.

Fixpoint snoc (l: list ascii) (v: ascii) : list ascii :=
  match l with
  | nil => v :: nil
  | h :: t => h :: (snoc t v)
  end.

Fixpoint rev (l: list ascii) : list ascii :=
  match l with
  | nil => nil
  | h :: t => snoc (rev t) h
  end.

Fixpoint uniq_i (chars : list ascii) : bool :=
  match chars with
    | nil => true
    | x :: xs => 
      if contain x xs
        then false
        else uniq_i xs
  end.

Definition uniq (str : string) : bool :=
  uniq_i (list_of_string str).

配列の先頭に付与する場合は帰納法で素直に解けるんですが、appendする場合は素直にいかない。
パターンマッチさせる場合 x::xsのように先頭でマッチさせるような関数を書いているのが原因だけど、配列の後尾から帰納的証明が行えるような機能が必要に思う。

証明は配列にappendした際の性質 in_app_or_congtain がキモ。

(* 配列に要素をappendした際の重要な補題 rev系の証明では必須 *)
Lemma in_app_or_contain:
  forall (l : list ascii) (a b : ascii),
    contain a (snoc l b) = (contain a l) || eqc b a.
Proof.
  intros l b a.
  induction l.
  simpl.
  case (eqc a b).
  reflexivity.
  reflexivity.
  simpl.
  rewrite -> IHl.
  case (eqc a0 b).
  reflexivity.
  reflexivity.
Qed.

証明の全容は
https://gist.github.com/4243787
にあります。
最後の定理が目的のものです。