Require MinMJ_theta.
Require MinMJ_psi.

(* Because the bald statement of the proof has the wrong type
inferred, we define the lemmas individually and unfold them after
applying induction. *)

Definition psthids :M->Prop :=
[m:M]((psi (theta m)) = m).

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

(* Now we actually state the lemma. *)

Lemma psthid : ((m:M)(psthids m))/\((ms:Ms)(psth'ps's ms)).

Lemma psitheta:
	(m:M)((psi(theta m))=m).

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