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

(Apply M_Ms_ind; Unfold psthids ; Unfold psth'ps's ; Intros).
(Rewrite -> th1; Exact (H (var v))).

(Rewrite -> th2; Rewrite -> ps1; Rewrite -> H; Auto).

(Rewrite -> th3; Rewrite -> ps2; Auto).

(Rewrite -> th4; Rewrite -> (H0 (ap a (theta m))); Rewrite -> ps3;
 Rewrite -> H; Auto).
Save.

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

Cut ((m:M)(psthids m))/\((ms:Ms)(psth'ps's ms)).
Unfold psthids; Intros; Case H; Auto.
Apply psthid.
Save.

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

Cut ((m:M)(psthids m))/\((ms:Ms)(psth'ps's ms)).
Unfold psth'ps's; Intros; Case H; Auto.
Apply psthid.
Save.