Variable P A : Type.
Variable empty : P.
Variable push : A -> P -> P.

Inductive FP : P -> Prop := 
   FPe : FP empty
 | Fpp : forall a p, FP p -> FP (push a p).

Inductive L : P -> nat -> Prop := 
 | Le : L empty O
 | Lp : forall a p n, L p n -> L (push a p) (1+n).

Lemma LFP : forall p n, L p n -> FP p.
Proof.
induction 1.
apply FPe.
apply Fpp.
assumption.
Qed.

Lemma FPL : forall p, FP p -> exists n, L p n. 
Proof.
induction 1.
exists O.
apply Le.
destruct IHFP as (n,H1).
exists (1+n).
apply Lp; assumption.
Qed.

Lemma LPinv0 : forall p, L p 0 -> p = empty.
Proof.
intros.
inversion H.
trivial.
Qed.

Lemma LPinvn0 : forall p n, L p (1+n) -> p <> empty.
Proof.
intros.
inversion H.
Abort.

Lemma LPinv : forall p n, L p (1+n) -> exists a q, p = push a q.
Proof.
intros.
inversion H.
exists a.
exists p0; trivial.
Qed.