(* (c) 2017, Jonas Kaiser *)

Require Import Omega List Program.Equality.
Require Import lib sysf lambda2.

Set Implicit Arguments.

Definition vrel := list (var * var).

Definition vr (R : vrel) (x y : var) : Prop := In (x,y) R.

Definition vrm (R : vrel) (xi zeta : var -> var) : vrel := map (fun p => (xi (fst p), zeta (snd p))) R.

Lemma vr_map R xi zeta x x' y y' : vr R x y -> xi x = x' -> zeta y = y' -> vr (vrm R xi zeta) x' y'.
Proof. intros. unfold vr, vrm. apply in_map_iff. exists (x,y). auto. Qed.

Lemma vr_unmap R xi zeta x y : vr (vrm R xi zeta) x y -> exists x' y', xi x' = x /\ zeta y' = y /\ vr R x' y'.
Proof.
  unfold vr, vrm. intros H. apply in_map_iff in H. destruct H as [[x' y'] [E L]].
  simpl in E. inversion E; subst. exists x', y'. auto.
Qed.

Lemma vrm_comb R xi zeta rho theta : vrm (vrm R xi zeta) rho theta = vrm R (xi >>> rho) (zeta >>> theta).
Proof. induction R; trivial. destruct a; simpl. congruence. Qed.

Lemma vr_app_or R1 R2 x y : vr (R1 ++ R2) x y -> vr R1 x y \/ vr R2 x y.
Proof. apply in_app_or. Qed.

Lemma vr_left_app R1 R2 x y : vr R1 x y -> vr (R1 ++ R2) x y.
Proof. intros. apply in_or_app. now left. Qed.

Lemma vr_right_app R1 R2 x y : vr R2 x y -> vr (R1 ++ R2) x y.
Proof. intros. apply in_or_app. now right. Qed.

Lemma vrm_app R1 R2 xi zeta : vrm (R1 ++ R2) xi zeta = vrm R1 xi zeta ++ vrm R2 xi zeta.
Proof. apply map_app. Qed.

(* R functional *)
Definition vr_func (R : vrel) := forall x y1 y2 : var, vr R x y1 -> vr R x y2 -> y1 = y2.

Lemma vr_func_nil : vr_func nil.
Proof. intros x y1 y2 H. destruct H. Qed.

Lemma vr_func_rs R : vr_func R -> vr_func (vrm R id (+1)).
Proof.
  intros Rf x y1 y2 H1 H2.
  destruct (vr_unmap _ _ _ _ _ H1) as [x' [y1' [Ex' [Ey1' V']]]].
  destruct (vr_unmap _ _ _ _ _ H2) as [x'' [y2' [Ex'' [Ey2' V'']]]].
  asimpl in *. subst. now rewrite (Rf _ _ _ V' V'').
Qed.

Lemma vr_func_ext R : vr_func R -> vr_func ((0,0) :: vrm R (+1) (+1)).
Proof.
  intros Rf x y1 y2 [E1|H1]%in_inv [E2|H2]%in_inv.
  - congruence.
  - exfalso. destruct (vr_unmap _ _ _ _ _ H2) as [xc [_ [E _]]].
    subst. discriminate E1.
  - exfalso. destruct (vr_unmap _ _ _ _ _ H1) as [xc [_ [E _]]].
    subst. discriminate E2.
  - destruct (vr_unmap _ _ _ _ _ H1) as [x' [y1' [Ex' [Ey1' V1]]]].
    destruct (vr_unmap _ _ _ _ _ H2) as [x'' [y2' [Ex'' [Ey2' V2]]]].
    subst. inversion Ex''. subst. now rewrite (Rf _ _ _ V1 V2).
Qed.

(* R injective *)
Definition vr_inj (R : vrel) := forall x1 x2 y : var, vr R x1 y -> vr R x2 y -> x1 = x2.

Lemma vr_inj_nil : vr_inj nil.
Proof. intros x y1 y2 H. destruct H. Qed.

Lemma vr_inj_rs R : vr_inj R -> vr_inj (vrm R id (+1)).
Proof.
  intros Rf x1 x2 y H1 H2.
  destruct (vr_unmap _ _ _ _ _ H1) as [x' [y1' [Ex' [Ey1' V1]]]].
  destruct (vr_unmap _ _ _ _ _ H2) as [x'' [y2' [Ex'' [Ey2' V2]]]].
  asimpl in *. subst. inversion Ey2'; subst. now rewrite (Rf _ _ _ V1 V2).
Qed.

Lemma vr_inj_ext R : vr_inj R -> vr_inj ((0,0) :: vrm R (+1) (+1)).
Proof.
  intros Rf x y1 y2 [E1|H1]%in_inv [E2|H2]%in_inv.
  - congruence.
  - exfalso. destruct (vr_unmap _ _ _ _ _ H2) as [_ [y [_ [E _]]]].
    subst. discriminate E1.
  - exfalso. destruct (vr_unmap _ _ _ _ _ H1) as [_ [y [_ [E _]]]].
    subst. discriminate E2.
  - destruct (vr_unmap _ _ _ _ _ H1) as [x1' [y' [Ex1' [Ey' V1]]]].
    destruct (vr_unmap _ _ _ _ _ H2) as [x2' [y'' [Ex2'' [Ey'' V2]]]].
    subst. inversion Ey''. subst. now rewrite (Rf _ _ _ V1 V2).
Qed.

Inductive tyrel (R : vrel) : typeF -> termL -> Prop :=
| tyrel_var x y : vr R x y -> tyrel R (TyVarF x) (VarL y)
| tyrel_imp A B a b : tyrel R A a -> tyrel (vrm R id (+1)) B b -> tyrel R (ImpF A B) (ProdL a b)
| tyrel_all A a : tyrel ((0,0) :: vrm R (+1) (+1)) A a -> tyrel R (AllF A) (ProdL (SortL Prp) a).

Lemma tyrel_func R A a1 a2 : vr_func R -> tyrel R A a1 -> tyrel R A a2 -> a1 = a2.
Proof.
  intros Rf H. revert a2. induction H; intros a' J; inv J.
  - now rewrite (Rf _ _ _ H H1).
  - pose proof (vr_func_rs Rf) as H'. f_equal; auto.
  - pose proof (vr_func_ext Rf) as H'. f_equal; auto.
Qed.

Lemma tyrel_inj R A1 A2 a : vr_inj R -> tyrel R A1 a -> tyrel R A2 a -> A1 = A2.
Proof.
  intros Ri H. revert A2. induction H; intros A' J; inv J.
  - now rewrite (Ri _ _ _ H H2).
  - pose proof (vr_inj_rs Ri) as Ri'. f_equal; auto.
  - exfalso. ainv.
  - exfalso. ainv.
  - pose proof (vr_inj_ext Ri) as Ri'. f_equal; auto.
Qed.

Definition vr_tyctx_fl N R Gamma := forall x, x < N -> exists y, vr R x y /\ atnd Gamma y (SortL Prp).

Definition vr_tyctx_fl_nil R Gamma : vr_tyctx_fl 0 R Gamma.
Proof. intros x H. omega. Qed.

Lemma vr_tyctx_fl_rs N R Gamma a : vr_tyctx_fl N R Gamma -> vr_tyctx_fl N (vrm R id (+1)) (a :: Gamma).
Proof.
  intros VC x Lx. specialize (VC _ Lx). destruct VC as [y [Rxy Ly]].
  exists (S y). split.
  - eapply vr_map; eauto.
  - econstructor; eauto.
Qed.

Lemma vr_tyctx_fl_ext N R Gamma : vr_tyctx_fl N R Gamma -> vr_tyctx_fl (1 + N) ((0,0) :: (vrm R (+1) (+1))) ((SortL Prp) :: Gamma).
Proof.
  intros VC [|x] Lx.
  - exists 0. split.
    + left; auto.
    + constructor; trivial.
  - apply lt_S_n in Lx. specialize (VC _ Lx). destruct VC as [y [Rxy Ly]]. exists (S y). split.
    + right. now apply (vr_map _ _ _ _ _ Rxy).
    + econstructor; eauto.
Qed.

Lemma tyrel_fl_tot_pres N A : istyF N A -> forall R Gamma, vr_tyctx_fl N R Gamma -> exists a, tyrel R A a /\ typingL Gamma a (SortL Prp).
Proof.
  intros H; induction H; intros R Gamma VC.
  - destruct (VC _ H) as [y [Rxy Ly]]. exists (VarL y). eauto using tyrel, typingL.
  - destruct (IHistyF1 _ _ VC) as [a [Ra Ta]].
    pose proof (vr_tyctx_fl_rs a VC) as VC'.
    destruct (IHistyF2 _ _ VC') as [b [Rb Tb]].
    exists (ProdL a b). split; econstructor; eauto.
  - apply vr_tyctx_fl_ext in VC. specialize (IHistyF _ _ VC). destruct IHistyF as [a [Ra Ta]].
    exists (ProdL (SortL Prp) a). split.
    + now constructor.
    + econstructor; eauto using typingL_ax.
Qed.

Definition vr_tyctx_lf N R Gamma := forall y, atnd Gamma y (SortL Prp) -> exists x, vr R x y /\ x < N.

Definition vr_tyctx_lf_nil N R : vr_tyctx_lf N R nil.
Proof. intros x H. ainv. Qed.

Lemma vr_tyctx_lf_rs N R Gamma a : vr_tyctx_lf N R Gamma -> typingL Gamma a (SortL Prp) -> vr_tyctx_lf N (vrm R id (+1)) (a :: Gamma).
Proof.
  intros VC Ta [|x] Lx; ainv. apply sortL_ren in H0; subst.
  specialize (VC _ H2). destruct VC as [x' [Rx'x Lx']]. exists x'; split; trivial.
  eapply vr_map; eauto.
Qed.

Lemma vr_tyctx_lf_ext N R Gamma : vr_tyctx_lf N R Gamma -> vr_tyctx_lf (1 + N) ((0,0) :: (vrm R (+1) (+1))) ((SortL Prp) :: Gamma).
Proof.
  intros VC [|x] Lx.
  - exists 0. split.
    + left; auto.
    + omega.
  - ainv. apply sortL_ren in H0; subst. destruct (VC _ H2) as [x' [Rx'x Lx']]. exists (S x'). split.
    + right. now apply (vr_map _ _ _ _ _ Rx'x).
    + omega.
Qed.

Lemma tyrel_lf_tot_pres Gamma a : typingL Gamma a (SortL Prp) -> forall R N, vr_tyctx_lf N R Gamma -> exists A, tyrel R A a /\ istyF N A.
Proof.
  intros H. depind H; intros R N VC.
  - destruct (VC _ H) as [x' [Rx'x Lx']]. exists (TyVarF x'); split; constructor; trivial.
  - specialize (IHtypingL2 (eq_refl _)). destruct u.
    + (* imp *) specialize (IHtypingL1 (eq_refl _) _ _ VC).
      destruct IHtypingL1 as [A [RA TA]]. apply vr_tyctx_lf_rs with (a:=a) in VC; trivial.
      destruct (IHtypingL2 _ _ VC) as [B [RB TB]]. exists (ImpF A B). split; now constructor.
    + (* all *) clear IHtypingL1. apply typingL_typ_degenerate in H; subst. apply vr_tyctx_lf_ext in VC.
      destruct (IHtypingL2 _ _ VC) as [B [RB TB]]. exists (AllF B). split; now constructor.
  - exfalso. apply typingL_propagation in H. destruct H as [EX | [u TProd]]; [discriminate EX|].
    inversion TProd. subst. pose proof (typingL_beta H0 H5) as HX. rewrite <- H1 in HX. ainv.
Qed.

(* CML for tyrel *)

Lemma tyrel_ren R A a xi zeta : tyrel R A a -> tyrel (vrm R xi zeta) A.[ren xi] a.[ren zeta].
Proof.
  intros H; revert xi zeta; induction H; intros xi zeta.
  - constructor. eapply vr_map; eauto.
  - constructor; auto. rewrite vrm_comb. asimpl. specialize (IHtyrel2 xi (upren zeta)).
    rewrite vrm_comb in IHtyrel2. now asimpl in IHtyrel2.
  - constructor. rewrite vrm_comb. asimpl. specialize (IHtyrel (upren xi) (upren zeta)).
    simpl in IHtyrel. rewrite vrm_comb in IHtyrel. now asimpl in IHtyrel.
Qed.

Lemma tyrel_weaken R1 R2 A a x y : tyrel (R1 ++ R2) A a -> tyrel (R1 ++ (x,y) :: R2) A a.
Proof.
  intros H; revert x y. depind H; intros z w.
  - constructor. destruct (vr_app_or _ _ _ _ H).
    + now apply vr_left_app.
    + apply vr_right_app. now right.
  - constructor; auto. rewrite vrm_app. simpl. apply IHtyrel2. rewrite vrm_app. apply JMeq_refl.
  - constructor; auto. rewrite vrm_app. simpl. rewrite app_comm_cons. apply IHtyrel. rewrite vrm_app.
    rewrite <- app_comm_cons. apply JMeq_refl.
Qed.

Corollary tyrel_weaken_hd R A a x y : tyrel R A a -> tyrel ((x,y) :: R) A a.
Proof. intros H. rewrite <- (@app_nil_l _ R) in H. eapply tyrel_weaken in H. eauto. Qed.

Lemma tyrel_unmap R A a xi zeta : tyrel (vrm R xi zeta) A a -> exists A' a', A = A'.[ren xi] /\ a = a'.[ren zeta] /\ tyrel R A' a'.
Proof.
  intros H; depind H.
  - destruct (vr_unmap _ _ _ _ _ H) as [x' [y' [Ex [Ey J]]]]. exists (TyVarF x'), (VarL y'); asimpl; subst.
    repeat split; trivial. now constructor.
  - specialize (IHtyrel1 _ _ _ (eq_refl _)). destruct IHtyrel1 as [A' [a' [EA [Ea RAa]]]].
    rewrite vrm_comb in IHtyrel2. specialize (IHtyrel2 _ _ _ (eq_refl _)).
    destruct IHtyrel2 as [B' [b' [EB [Eb RBb]]]]. exists (ImpF A' B'), (ProdL a' b'.[ren (+1)]).
    apply tyrel_ren with (xi:=id)(zeta:=(+1)) in RBb. asimpl in *. repeat split; try congruence. now constructor.
  - specialize (IHtyrel ((0,0) :: (vrm R (+1) (+1))) (upren xi) (upren zeta)).
    simpl vrm in IHtyrel. repeat rewrite vrm_comb in IHtyrel. asimpl in IHtyrel.
    specialize (IHtyrel (eq_refl _)). destruct IHtyrel as [A' [a' [EA [Ea RAa]]]].
    exists (AllF A'), (ProdL (SortL Prp) a'). asimpl in *. repeat split; try congruence. now constructor.
Qed.

Definition cm_tyrel R1 sigma tau R2 := forall x y, vr R1 x y -> tyrel R2 (sigma x) (tau y).

Lemma cm_tyrel_rs R1 sigma tau R2 : cm_tyrel R1 sigma tau R2 -> cm_tyrel (vrm R1 id (+1)) sigma (up tau) (vrm R2 id (+1)).
Proof.
  intros CM x y Rxy. apply vr_unmap in Rxy. destruct Rxy as [x' [y' [Ex [Ey J]]]].
  subst; asimpl in *. apply CM in J. apply tyrel_ren with (xi:=id) (zeta:=(+1)) in J. now asimpl in *.
Qed.

Lemma cm_tyrel_ext R1 sigma tau R2 : cm_tyrel R1 sigma tau R2 -> cm_tyrel ((0, 0) :: vrm R1 (+1) (+1)) (up sigma) (up tau) ((0, 0) :: vrm R2 (+1) (+1)).
Proof.
  intros CM x y [E|H]%in_inv.
  - inversion E; subst; asimpl. constructor. now left.
  - apply vr_unmap in H. destruct H as [x' [y' [Ex [Ey J]]]]. subst; asimpl.
    apply CM in J. apply tyrel_ren with (xi:=(+1)) (zeta := (+1)) in J. now apply tyrel_weaken_hd.
Qed.

Lemma tyrel_subst R1 A a : tyrel R1 A a -> forall sigma tau R2, cm_tyrel R1 sigma tau R2 -> tyrel R2 A.[sigma] a.[tau].
Proof.
  intros H; induction H; intros sigma tau R2 CM.
  - asimpl. auto.
  - pose proof (cm_tyrel_rs CM) as CM'. constructor; auto.
  - apply cm_tyrel_ext in CM. constructor; auto.
Qed.

Lemma cm_tyrel_beta R B b : tyrel R B b -> cm_tyrel ((0, 0) :: vrm R (+1) (+1)) (B .: ids) (b .: ids) R.
Proof.
  intros H x y [E|J]%in_inv.
  - inversion E; subst; asimpl. trivial.
  - destruct (vr_unmap _ _ _ _ _ J) as [x' [y' [Ex [Ey K]]]]; subst; asimpl.
    now constructor.
Qed.

Lemma tyrel_beta R A a B b : tyrel R B b -> tyrel ((0,0) :: vrm R (+1) (+1)) A a -> tyrel R A.[B/] a.[b/].
Proof. intros HB HA. eapply tyrel_subst; eauto using cm_tyrel_beta. Qed.

Inductive tmrel (Rty Rtm : vrel) : termF -> termL -> Prop :=
| tmrel_var x y : vr Rtm x y -> tmrel Rty Rtm (TmVarF x) (VarL y)
| tmrel_app s t a b : tmrel Rty Rtm s a -> tmrel Rty Rtm t b -> tmrel Rty Rtm (AppF s t) (AppL a b)
| tmrel_lam A s a b: tyrel Rty A a -> tmrel (vrm Rty id (+1)) ((0,0) :: vrm Rtm (+1) (+1)) s b -> tmrel Rty Rtm (LamF A s) (LamL a b)
| tmrel_tyspec s A a b : tmrel Rty Rtm s a -> tyrel Rty A b -> tmrel Rty Rtm (TySpecF s A) (AppL a b)
| tmrel_tyabs s a : tmrel ((0,0) :: vrm Rty (+1) (+1)) (vrm Rtm id (+1)) s a -> tmrel Rty Rtm (TyAbsF s) (LamL (SortL Prp) a).

(* VR disjoint on range *)
Definition vr_rdis (R1 R2 : vrel) := forall x1 x2 y : var, vr R1 x1 y -> vr R2 x2 y -> False.

Lemma vr_rdis_sym R1 R2 : vr_rdis R1 R2 -> vr_rdis R2 R1.
Proof. firstorder. Qed.

Lemma vr_rdis_l_nil R2 : vr_rdis nil R2.
Proof. intros x1 x2 y H. destruct H. Qed.

Lemma vr_rdis_r_nil R1: vr_rdis R1 nil.
Proof. apply vr_rdis_sym, vr_rdis_l_nil. Qed.

Lemma vr_rdis_rs_ext R1 R2 : vr_rdis R1 R2 -> vr_rdis (vrm R1 id (+1)) ((0, 0) :: vrm R2 (+1) (+1)).
Proof.
  intros VD x1 x2 y H1 H2.
  destruct (vr_unmap _ _ _ _ _ H1) as [x1' [y' [Ex [Ey Rx1y]]]]. asimpl in *. subst.
  destruct H2 as [E|H]; [discriminate E|].
  destruct (vr_unmap _ _ _ _ _ H) as [x2' [y'' [Ex [Ey Rx2y]]]]. asimpl in *. subst.
  inversion Ey; subst. destruct (VD _ _ _ Rx1y Rx2y).
Qed.

Lemma vr_rdis_ext_rs R1 R2 : vr_rdis R1 R2 -> vr_rdis ((0, 0) :: vrm R1 (+1) (+1)) (vrm R2 id (+1)).
Proof. intros H. now apply vr_rdis_sym, vr_rdis_rs_ext, vr_rdis_sym. Qed.

Lemma tyrel_tmrel_disjoint (Rty Rtm : vrel) A s a : vr_rdis Rty Rtm -> tyrel Rty A a -> tmrel Rty Rtm s a -> False.
Proof. intros VD H; revert s. induction H; intros s J; inversion J; subst. firstorder. Qed.

Lemma tmrel_func Rty Rtm s a1 a2 : vr_func Rty -> vr_func Rtm -> tmrel Rty Rtm s a1 -> tmrel Rty Rtm s a2 -> a1 = a2.
Proof.
  intros Rtyf Rtmf H. revert a2. induction H; intros a' J; inv J.
  - now rewrite (Rtmf _ _ _ H H1).
  - f_equal; auto.
  - pose proof (vr_func_rs Rtyf) as Hty. pose proof (vr_func_ext Rtmf) as Htm.
    f_equal; eauto using tyrel_func.
  - f_equal; eauto using tyrel_func.
  - pose proof (vr_func_ext Rtyf) as Hty. pose proof (vr_func_rs Rtmf) as Htm.
    f_equal; eauto using tyrel_func.
Qed.

Lemma tmrel_inj Rty Rtm s1 s2 a : vr_inj Rty -> vr_inj Rtm -> vr_rdis Rty Rtm -> tmrel Rty Rtm s1 a -> tmrel Rty Rtm s2 a -> s1 = s2.
Proof.
  intros Rtyi Rtmi VD H. revert s2. induction H; intros A' J; inv J.
  - now rewrite (Rtmi _ _ _ H H2).
  - f_equal; auto.
  - destruct (tyrel_tmrel_disjoint VD H5 H0).
  - pose proof (vr_inj_rs Rtyi) as Hty. pose proof (vr_inj_ext Rtmi) as Htm.
    pose proof (vr_rdis_rs_ext VD) as VD'. f_equal; eauto using tyrel_inj.
  - ainv.
  - destruct (tyrel_tmrel_disjoint VD H0 H5).
  - f_equal; eauto using tyrel_inj.
  - ainv.
  - pose proof (vr_inj_ext Rtyi) as Hty. pose proof (vr_inj_rs Rtmi) as Htm.
    pose proof (vr_rdis_ext_rs VD) as VD'. f_equal; auto.
Qed.

Definition vr_tmctx_fl Delta Rty Rtm Gamma := forall x A, atn Delta x A -> exists y a, tyrel Rty A a /\ vr Rtm x y /\ atnd Gamma y a.

Lemma vr_tmctx_fl_nil Rty Rtm Gamma : vr_tmctx_fl nil Rty Rtm Gamma.
Proof. intros x A H. ainv. Qed.

Lemma vr_tmctx_fl_rs_ext Delta Rty Rtm Gamma A a : vr_tmctx_fl Delta Rty Rtm Gamma -> tyrel Rty A a -> vr_tmctx_fl (A :: Delta) (vrm Rty id (+1)) ((0,0) :: (vrm Rtm (+1) (+1))) (a :: Gamma).
Proof.
  intros VC TyRAa [|x] B Lx.
  - ainv. exists 0, a.[ren (+1)]. apply tyrel_ren with (xi:=id)(zeta:=(+1)) in TyRAa. asimpl in TyRAa.
    split; trivial. split.
    + left; auto.
    + now constructor.
  - ainv. specialize (VC _ _ H3). destruct VC as [y [b [TyRBb [Rxy Ly]]]]. exists (S y), b.[ren (+1)].
    apply tyrel_ren with (xi:=id)(zeta:=(+1)) in TyRBb. asimpl in TyRBb. split; trivial. split.
    + right. eapply vr_map; eauto.
    + econstructor; eauto.
Qed.

Lemma vr_tmctx_fl_ext_rs Delta Rty Rtm Gamma : vr_tmctx_fl Delta Rty Rtm Gamma -> vr_tmctx_fl Delta..[ren (+1)] ((0,0) :: (vrm Rty (+1) (+1))) (vrm Rtm id (+1)) ((SortL Prp) :: Gamma).
Proof.
  intros VC x B Lx. destruct (mmap_atn Lx) as [B' [EB Lx']].
  specialize (VC _ _ Lx'). destruct VC as [y [b [TyRB'b [Rxy Ly]]]].
  exists (S y), b.[ren (+1)]. repeat split.
  - subst. apply tyrel_ren with (xi:=(+1))(zeta:=(+1)) in TyRB'b. now apply tyrel_weaken_hd.
  - eapply vr_map; eauto.
  - econstructor; eauto.
Qed.

Lemma tmrel_fl_tot_pres N Delta s A : typingF N Delta s A -> forall Rty Rtm Gamma, vr_func Rty -> vr_tyctx_fl N Rty Gamma -> vr_tmctx_fl Delta Rty Rtm Gamma -> exists a b, tyrel Rty A b /\ tmrel Rty Rtm s a /\ typingL Gamma a b /\ typingL Gamma b (SortL Prp).
Proof.
  intros H; induction H; intros Rty Rtm Theta RtyF VCty VCtm.
  - destruct (tyrel_fl_tot_pres H0 VCty) as [b [TyRb Tb]].
    destruct (VCtm _ _ H) as [y [b' [TyRb' [Rxy Ly]]]].
    pose proof (tyrel_func RtyF TyRb TyRb') as E. subst.
    exists (VarL y), b'. repeat split; trivial; econstructor; eauto.
  - specialize (IHtypingF1 _ _ _ RtyF VCty VCtm). destruct IHtypingF1 as [la [pr [TyRalpr [TmRsla [Tla Tpr]]]]].
    specialize (IHtypingF2 _ _ _ RtyF VCty VCtm). destruct IHtypingF2 as [c [a [TyRAa [TmRtc [Tc Ta]]]]].
    inversion TyRalpr; subst. destruct (tyrel_unmap _ _ _ H5) as [B' [b' [EB [Eb TyRBb]]]]. asimpl in *. subst.
    exists (AppL la c), b'. repeat split.
    + assumption.
    + now constructor.
    + assert (a = a0) by (eapply tyrel_func; eauto); subst. econstructor; eauto. autosubst.
    + inversion Tpr; subst. now apply typingL_sort_strengthen in H6.
      (* Note that this form of Strengthening is obtained via detour through System P ! *)
  - destruct (tyrel_fl_tot_pres H VCty) as [a [TyRa Ta]].
    eapply vr_tmctx_fl_rs_ext in VCtm; eauto.
    apply vr_tyctx_fl_rs with (a:=a) in VCty.
    apply vr_func_rs in RtyF.
    destruct (IHtypingF _ _ _ RtyF VCty VCtm) as [c [b [TyRBb [TmRsc [Tc Tb]]]]].
    exists (LamL a c), (ProdL a b). repeat split; econstructor; eauto.
  - specialize (IHtypingF _ _ _ RtyF VCty VCtm). destruct IHtypingF as [la [pr [TyRalpr [TmRsla [Tla Tpr]]]]].
    destruct (tyrel_fl_tot_pres H VCty) as [b [TyRBb Tb]]. inversion TyRalpr; subst.
    exists (AppL la b), a.[b/]. repeat split.
    + now apply tyrel_beta.
    + now constructor.
    + econstructor; eauto.
    + rewrite (sortL_add_subst (b .: ids)). eapply typingL_beta; eauto. now inversion Tpr; subst.
  - apply vr_tmctx_fl_ext_rs in VCtm.
    apply vr_tyctx_fl_ext in VCty.
    apply vr_func_ext in RtyF.
    destruct (IHtypingF _ _ _ RtyF VCty VCtm) as [c [b [TyRBb [TmRsc [Tc Tb]]]]].
    exists (LamL (SortL Prp) c), (ProdL (SortL Prp) b). repeat split; econstructor; eauto using typingL_ax.
Qed.

Definition vr_tmctx_lf Delta Rty Rtm Gamma := forall y a, atnd Gamma y a -> typingL Gamma a (SortL Prp) -> exists x A, tyrel Rty A a /\ vr Rtm x y /\ atn Delta x A.

Lemma vr_tmctx_lf_nil Delta Rty Rtm : vr_tmctx_lf Delta Rty Rtm nil.
Proof. intros y a H. ainv. Qed.

Lemma vr_tmctx_lf_rs_ext Delta Rty Rtm Gamma A a : vr_tmctx_lf Delta Rty Rtm Gamma -> tyrel Rty A a -> vr_tmctx_lf (A :: Delta) (vrm Rty id (+1)) ((0,0) :: (vrm Rtm (+1) (+1))) (a :: Gamma).
Proof.
  intros VC TyRAa [|y] b Ly Tb.
  - ainv. exists 0, A. repeat split.
    + apply tyrel_ren with (xi:=id)(zeta:=(+1)) in TyRAa. now asimpl in *.
    + now left.
    + constructor.
  - ainv. apply typingL_sort_strengthen in Tb. destruct (VC _ _ H2 Tb) as [x [A' [TyRA'a [Rxy Lx]]]].
    exists (S x), A'. repeat split.
    + apply tyrel_ren with (xi:=id)(zeta:=(+1)) in TyRA'a. now asimpl in *.
    + right. eapply vr_map; eauto.
    + now constructor.
Qed.

Lemma vr_tmctx_lf_ext_rs Delta Rty Rtm Gamma : vr_tmctx_lf Delta Rty Rtm Gamma -> vr_tmctx_lf Delta..[ren (+1)] ((0,0) :: (vrm Rty (+1) (+1))) (vrm Rtm id (+1)) ((SortL Prp) :: Gamma).
Proof.
  intros VC [|y] b Ly Tb; inversion Ly; subst.
  - asimpl in *. destruct (typingL_prp_prp_contra Tb).
  - apply typingL_sort_strengthen in Tb. destruct (VC _ _ H2 Tb) as [x [A' [TyRA'a [Rxy Lx]]]].
    exists x, A'.[ren (+1)]. repeat split.
    + apply tyrel_ren with (xi:=(+1))(zeta:=(+1)) in TyRA'a. now apply tyrel_weaken_hd.
    + eapply vr_map; eauto.
    + eapply atn_mmap; eauto.
Qed.

Lemma tmrel_lf_tot_pres Gamma a b : typingL Gamma b (SortL Prp) -> typingL Gamma a b -> forall Rty Rtm N Delta, vr_inj Rty -> vr_tyctx_lf N Rty Gamma -> vr_tmctx_lf Delta Rty Rtm Gamma -> exists s A, tyrel Rty A b /\ tmrel Rty Rtm s a /\ typingF N Delta s A /\ istyF N A.
Proof.
  intros Tb H. induction H; intros Rty Rtm N Delta VI VCty VCtm; ainv.
  - destruct (VCtm _ _ H Tb) as [x' [A [TyRAa [Rx'x Lx]]]]. exists (TmVarF x'), A.
    destruct (tyrel_lf_tot_pres Tb VCty) as [A' [TyRA'a TA]].
    assert (A = A') by (eapply tyrel_inj; eauto); subst.
    repeat split; trivial; now constructor.
  - pose proof (typingL_propagation H) as J. destruct J as [E|[u Tpr]]; [discriminate E|].
    inversion Tpr; subst. specialize (IHtypingL1 Tpr _ _ _ _ VI VCty VCtm).
    destruct IHtypingL1 as [f [F [TyRFpr [TmRfa [Tf TF]]]]]. destruct u0.
    + (* AppF *) specialize (IHtypingL2 H4 _ _ _ _ VI VCty VCtm).
      destruct IHtypingL2 as [s [C [TyRCc [TmRsb [Ts TC]]]]].
      inversion TyRFpr; subst; [|inversion TyRCc].
      exists (AppF f s), B. repeat split.
      * destruct (tyrel_unmap _ _ _ H7) as [B' [d' [EB [Ed TyRB'd']]]]. subst; now asimpl in *.
      * now constructor.
      * assert (A = C) by (eapply tyrel_inj; eauto); subst. econstructor; eauto.
      * now inversion TF; subst.
    + (* TySpecF *) apply typingL_typ_degenerate in H4; subst. clear IHtypingL2.
      destruct (tyrel_lf_tot_pres H0 VCty) as [B [TyRBb TB]].
      inversion TyRFpr; subst; [inversion H4|].
      exists (TySpecF f B), (A.[B/]). repeat split.
      * now apply tyrel_beta.
      * now constructor.
      * econstructor; eauto.
      * inversion TF; subst. now apply istyF_beta.
  - clear IHtypingL1 IHtypingL2. specialize (IHtypingL3 H0). destruct u.
    + (* LamF *) destruct (tyrel_lf_tot_pres H VCty) as [A [TyRAa TA]].
      eapply vr_tyctx_lf_rs in VCty; eauto. eapply vr_tmctx_lf_rs_ext in VCtm; eauto. apply vr_inj_rs in VI.
      specialize (IHtypingL3 _ _ _ _ VI VCty VCtm). destruct IHtypingL3 as [s [B [TyRBc [TmRsb [Ts TB]]]]].
      exists (LamF A s), (ImpF A B). repeat split; now constructor.
    + (* TyAbsF *) apply typingL_typ_degenerate in H; subst.
      eapply vr_tyctx_lf_ext in VCty. apply vr_tmctx_lf_ext_rs in VCtm. apply vr_inj_ext in VI.
      specialize (IHtypingL3 _ _ _ _ VI VCty VCtm). destruct IHtypingL3 as [s [A [TyRAc [TmRsb [Ts TA]]]]].
      exists (TyAbsF s), (AllF A). repeat split; now constructor.
Qed.

(* Instances for closed judgments, full characterisation of A ~ a and s ~~ b *)

Corollary tyrel_functional A a a' : tyrel nil A a -> tyrel nil A a' -> a = a'.
Proof. intros. eapply tyrel_func; eauto using vr_func_nil. Qed.

Corollary tyrel_injective A A' a : tyrel nil A a -> tyrel nil A' a -> A = A'.
Proof. intros. eapply tyrel_inj; eauto using vr_inj_nil. Qed.

Corollary tyrel_fl_total_preserving A : istyF 0 A <-> exists a, tyrel nil A a /\ typingL nil a (SortL Prp).
Proof.
  split.
  - intros. eapply tyrel_fl_tot_pres; eauto using vr_tyctx_fl_nil.
  - intros [a [RA Ta]]. apply tyrel_lf_tot_pres with (R:=nil) (N:=0) in Ta; auto using vr_tyctx_lf_nil.
    destruct Ta as [A' [RA' H]]. now rewrite (tyrel_injective RA RA').
Qed.

Corollary tyrel_lf_total_preserving a : typingL nil a (SortL Prp) <-> exists A, tyrel nil A a /\ istyF 0 A.
Proof.
  split.
  - intros. eapply tyrel_lf_tot_pres; eauto using vr_tyctx_lf_nil.
  - intros [A [Ra TA]]. apply tyrel_fl_tot_pres with (R:=nil) (Gamma:=nil) in TA; auto using vr_tyctx_fl_nil.
    destruct TA as [a' [Ra' H]]. now rewrite (tyrel_functional Ra Ra').
Qed.

Corollary tmrel_functional s a a' : tmrel nil nil s a -> tmrel nil nil s a' -> a = a'.
Proof. intros. eapply tmrel_func; eauto using vr_func_nil. Qed.

Corollary tmrel_injective s s' a : tmrel nil nil s a -> tmrel nil nil s' a -> s = s'.
Proof. intros. eapply tmrel_inj; eauto using vr_inj_nil, vr_rdis_r_nil. Qed.

Corollary tmrel_fl_total_preserving s A : typingF 0 nil s A <-> exists a b, tyrel nil A b /\ tmrel nil nil s a /\ typingL nil a b /\ typingL nil b (SortL Prp).
Proof.
  split.
  - intros. eapply tmrel_fl_tot_pres; eauto using vr_func_nil, vr_tyctx_fl_nil, vr_tmctx_fl_nil.
  - intros [a [b [RA [Rs [Ta Tb]]]]]. eapply tmrel_lf_tot_pres with (Rtm:=nil) (N:=0) (Delta:=nil) in Ta;
                                        eauto using vr_inj_nil, vr_tyctx_lf_nil, vr_tmctx_lf_nil.
    destruct Ta as [s' [A' [RA' [Rs' [Ts' TA']]]]]. now rewrite (tyrel_injective RA RA'), (tmrel_injective Rs Rs').
Qed.

Corollary tmrel_lf_total_preserving a b : typingL nil b (SortL Prp) /\ typingL nil a b <-> exists s A, tyrel nil A b /\ tmrel nil nil s a /\ typingF 0 nil s A /\ istyF 0 A.
Proof.
  split.
  - intros [Tb Ta]. eapply tmrel_lf_tot_pres; eauto using vr_inj_nil, vr_tyctx_lf_nil, vr_tmctx_lf_nil.
  - intros [s [A [Rb [Ra [Ts TA]]]]]. eapply tmrel_fl_tot_pres with (Rtm:=nil) (Gamma:=nil) in Ts;
                                        eauto using vr_func_nil, vr_tyctx_fl_nil, vr_tmctx_fl_nil.
    destruct Ts as [a' [b' [Rb' [Ra' [Ta' Tb']]]]]. now rewrite (tyrel_functional Rb Rb'), (tmrel_functional Ra Ra').
Qed.