Require MinMJ_Hyps.

Inductive
    In_Hyps : nat->F->Hyps->Prop :=
	inhyps_base : (P:F)(h:Hyps)
			(In_Hyps O P (Add_Hyp P h)) |
	inhyps_rec : (n:nat)(P,Q:F)(h:Hyps)
			(In_Hyps n P h)->
			 (In_Hyps (S n) P (Add_Hyp Q h)).

Definition V :Set := nat.

Lemma In_lt :
	(h:Hyps)(x:V)(P:F)
	 (In_Hyps x P h)->
	  (lt x (Len_Hyps h)).

(Induction h; Clear  h; Intros).
Inversion H.

Inversion_clear H0.
(Simpl; Auto).

(Simpl; Apply lt_S; Apply (H n P); Auto).
Save.

Hint inhyps_base.
Hint inhyps_rec.