Require MinMJ_theta.
Require MinMJ_psi.

Definition thpsids :N->Prop :=
[n:N]((theta (psi n)) = n).

Definition thps'th's :A->Prop :=
[a:A](ms:Ms)((theta (psi' a ms)) = (theta' a ms)).

(*Now the actual proof *)

Lemma thpsid : ((n:N)(thpsids n))/\((a:A)(thps'th's a)).

Lemma thetapsi:
	(n:N)((theta(psi n)) = n).

Lemma thetapsi'theta':
	(a:A)(ms:Ms)((theta (psi' a ms)) = (theta' a ms)).