The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

  Let us consider a type of finite or infinite lists :

Variable (A:Type).

CoInductive LList :=
  | LNil: LList
  | LCons : A -> LList -> LList.


Inductive Finite : LList -> Prop :=
  |Finite_LNil: Finite LNil
  |Finite_LCons   : forall a l, Finite l-> Finite (LCons a l).


Is it possible to prove unicity of proofs of Finite ?

Goal forall l (H H0:Finite l), H=H0 ?

Pierre