Require MinMJ_Exchange.

Lemma V_Exchange_inv :
	(x:V)(i,j:nat)
	 i=j->
	  (V_Exchange i (V_Exchange j x))=x.

Lemma L_Exchange_inv :
	(l:L)(i,j:nat)
	 i=j->
	  (L_Exchange i (L_Exchange j l))=l.