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)).