Require MinMJ_M.
Require MinMJ_N.

Fixpoint
    psi [n:N]:M :=
	<M>Case n of
	    (* lam n *)[n:N]
		(lambda (psi n))
	    (* an a *)[a:A]
		(psi' a mnil)
end with
    psi' [a:A]:Ms->M :=
	[ms:Ms]<M>Case a of
	    (* ap a n *)[a':A][n:N]
		(psi' a' (mcons (psi n) ms))
	    (* var v *)[x:V]
		(sc x ms)
end.

Lemma ps1 : (n:N)((psi (lam n)) = (lambda (psi n))).
Trivial.
Save.

Lemma ps2 : (a:A)((psi (an a)) = (psi' a mnil)).
Trivial.
Save.

Lemma ps3 : (a:A)(n:N)(ms:Ms)((psi' (ap a n) ms) 
	= (psi' a (mcons (psi n) ms))).
Trivial.
Save.

Lemma ps4 : (x:V)(ms:Ms)((psi' (var x) ms) = (sc x ms)).
Trivial.
Save.