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

(Apply N_A_ind; Unfold thpsids ; Unfold thps'th's thpsids ; Intros).
(Rewrite -> ps1; Rewrite -> th2; Rewrite -> H; Auto).

(Rewrite -> ps2; Exact (H mnil)).

(Rewrite -> ps3; Rewrite -> (H (mcons (psi n) ms)); Rewrite -> th4;
 Rewrite -> H0; Auto).

(Rewrite -> ps4; Rewrite -> th1; Auto).
Save.

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

Cut ((n:N)(thpsids n))/\((a:A)(thps'th's a)).
Unfold thpsids; Intros; Case H; Auto.
Apply thpsid.
Save.

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

Cut ((n:N)(thpsids n))/\((a:A)(thps'th's a)).
Unfold thps'th's; Intros; Case H; Auto.
Apply thpsid.
Save.