Require MinMJ_M.
Require MinMJ_N.

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

(* Theta1' has its arguments in the wrong order so define theta'
in the same order as psi' later for ease of human parsing and consistency. *)

Recursive Definition theta' : A -> Ms -> N :=
a ms => (theta1' ms a).

Lemma th1 : (x:V)(ms:Ms)((theta (sc x ms)) = (theta' (var x) ms)).
Trivial.
Save.

Lemma th2 : (m:M)((theta (lambda m)) = (lam (theta m))).
Trivial.
Save.

Lemma th3 : (a:A)((theta' a mnil) = (an a)).
Trivial.
Save.

Lemma th4 : (m:M)(ms:Ms)(a:A)((theta' a (mcons m ms)) 
	= (theta' (ap a (theta m)) ms)).
Trivial.
Save.