The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 03.10.2013 14:35, schrieb Cedric Auger:
> A n (l : list A) (x y : NList_ n l), x = y.

Jup. There might be a simpler proof, but here is one:

Lemma NList_Unique {A} (l : list A) n (y : NList_ n l): match n return 
NList_ n l -> Prop with
  | 0 => fun y => Base l = y
  | S n' =>
    match l with
    | nil => fun y => False
    | cons a l' => fun y => exists x : NList_ n' l', Cons n' l' a x = y
    end
  end y.
induction y ; auto.
exists y ; auto.
Qed.

Goal forall A n (l : list A) (x y : NList_ n l), x = y.
induction x.
  apply (NList_Unique l).

  intros y.
  destruct (NList_Unique (a :: l) (S n) y) as [x' P].
  now rewrite IHx with x'.
Qed.