Definition rall U r := App (Lam r U) (joker U).
Definition rlet U s r := App (Lam r U) s.

Fixpoint lam_params (c : expr -> recipe) (d : expr) : recipe :=
  match d with
  | ETLam d => TLam (lam_params c d)
  | ELam d π => Lam (lam_params c d) π
  | d => c d
  end.

Fixpoint all_params (c : expr -> recipe) (d : expr) : recipe :=
  match d with
  | ETLam d => TAll (all_params c d)
  | ELam d π => rall π (all_params c d)
  | d => c d
  end.

Fixpoint VC (p d : bool) (e : expr) : recipe :=
  match e with
  | EVar h => if p then Var h else Neu (Var h)
  | ETApp e s => TApp (VC p d e) s
  | EApp e1 e2 => App (VC p d e1) (VC p d e2)
  | ETLam e => TLam (VC p d e)
  | ELam e π => And (Lam (VC p d e) π) (Neu (Lam (VC (~~ p) (~~ d) e) π))
  | EBar B e => VC (sel B p d) (sel B p d) e
  | EDef e B π b =>
      rlet π (rall π (lam_params (VC true false) b))
             (And (VC p d e) (all_params (VC false (sel B p d)) b))
  end.

Lemma has_type_rall Γ a U r :
  [ U .: Γ, a, a ⊢ r :- Void ] ->
  [ Γ, a, a ⊢ rall U r :- Void ].
Proof.
  move=> *.
  apply ty_app with U.
  - by constructor.
  - by apply has_type_joker_gen; constructor.
Qed.

Lemma has_type_VC :
  (forall Γ e π, [ Γ ⊩ e :- π ] ->
     forall p d a, [ Γ, a, a ⊢ VC p d e :- π ]) /\
  (forall Γ π b, [ Γ ⊩ π ↦ b ] ->
     forall p d a,
     [ Γ, a, a ⊢ lam_params (VC p d) b :- π ] /\
     [ Γ, a, a ⊢ all_params (VC p d) b :- Void ]).
Proof.
  apply cty_cabs_mut=> //=; try by repeat constructor.
  - move=> > <- [] *; by repeat constructor.
  - move=> *.
    constructor=>//.
    by apply fv_plage_eq.
  - move=> ??? U V *.
    by apply ty_app with U.
  - move=> ??? U ?? ih1 ? ih2 *.
    apply ty_app with U.
    + repeat constructor=>//.
      by apply ih2.
    + apply ty_app with U.
      constructor.
      by apply ih2.
      by apply has_type_joker_gen; constructor.
  - move=> ? [] > hb ih *; try inv hb; split; apply ih.
  - move=> > ? ih *.
    split; constructor=>//; by apply ih.
  - move=> > ? ih *.
    split.
    + constructor. by apply ih.
    + by apply has_type_rall, ih.
Qed.

Corollary ty_VC p d a Γ e π :
  [ Γ ⊩ e :- π ] ->
  [ Γ, a, a ⊢ VC p d e :- π ].
Proof.
  move=> ?.
  by apply has_type_VC.
Qed.

Corollary ty_params p d a Γ π b :
  [ Γ ⊩ π ↦ b ] ->
  [ Γ, a, a ⊢ lam_params (VC p d) b :- π ] /\
  [ Γ, a, a ⊢ all_params (VC p d) b :- Void ].
Proof.
  move=> ?.
  by apply has_type_VC.
Qed.

Lemma VC_hsubst p d e θ :
  (VC p d e).|[θ] = VC p d e.|[θ].
Proof.
  have: forall e θ,
    [/\ forall p d, (VC p d e).|[θ] = VC p d e.|[θ],
        forall p d, (lam_params (VC p d) e).|[θ] = lam_params (VC p d) e.|[θ]
      & forall p d, (all_params (VC p d) e).|[θ] = all_params (VC p d) e.|[θ]].
  2: { by move=> /(_ e θ) [ + _ _ ]. }
  (* prove the generalization *)
  clear_all.
  elim.
  - by split=> -[].
  - move=> e ih s θ.
    have [h _ _] := ih θ.
    have {}h p d : (VC p d (ETApp e s)).|[θ] = VC p d (ETApp e s).|[θ]
      by rewrite /= h.
    by split.
  - move=> e1 ih1 e2 ih2 θ.
    have [h1 _ _] := ih1 θ.
    have [h2 _ _] := ih2 θ.
    have h p d : (VC p d (EApp e1 e2)).|[θ] = VC p d (EApp e1 e2).|[θ]
      by rewrite /= h1 h2.
    by split.
  - move=> e ih θ.
    have [h1 h2 h3] := ih (up θ).
    by split=> *; rewrite /= ?h1 ?h2 ?h3.
  - move=> e ih ? θ.
    have [h1 h2 h3] := ih θ.
    split=> *; rewrite /= ?h1 ?h2 ?h3 //=.
    rewrite /rall closedh_hsubst=>//.
    by apply closedh_joker.
  - move=> B e ih θ.
    have [h _ _] := ih θ.
    have {}h p d : (VC p d (EBar B e)).|[θ] = VC p d (EBar B e).|[θ]
      by rewrite /= h.
    by split.
  - move=> e ih1 B π b ih2 θ.
    have [h1 _ _] := ih1 θ.
    have [_ h2 h3] := ih2 θ.
    have h p d : (VC p d (EDef e B π b)).|[θ] = VC p d (EDef e B π b).|[θ].
    { rewrite /= h1 h2 h3.
      rewrite /rlet closedh_hsubst=>//.
      by apply closedh_joker. }
    by split.
Qed.

Lemma VC_ren p d e ξ :
  (VC p d e).[ren ξ] = VC p d e.[ren ξ].
Proof.
  have: forall e ξ,
        [/\ forall p d, (VC p d e).[ren ξ] = VC p d e.[ren ξ],
            forall p d, (lam_params (VC p d) e).[ren ξ] = lam_params (VC p d) e.[ren ξ]
          & forall p d, (all_params (VC p d) e).[ren ξ] = all_params (VC p d) e.[ren ξ]].
  2: { by move=> /(_ e ξ) [ + _ _ ]. }
  (* prove the generalization *)
  clear_all.
  elim.
  - by split=> -[].
  - move=> e ih s ξ.
    have [h _ _] := ih ξ.
    have {}h p d : (VC p d (ETApp e s)).[ren ξ] = VC p d (ETApp e s).[ren ξ]
      by rewrite /= h.
    by split.
  - move=> e1 ih1 e2 ih2 ξ.
    have [{}h1 _ _] := ih1 ξ.
    have [{}h2 _ _] := ih2 ξ.
    have h p d : (VC p d (EApp e1 e2)).[ren ξ] = VC p d (EApp e1 e2).[ren ξ]
      by rewrite /= h1 h2.
    by split.
  - move=> e ih ξ.
    have [h1 h2 h3] := ih ξ.
    by split=> *; rewrite /= ?h1 ?h2 ?h3.
  - move=> e ih ? ξ.
    have [h1 h2 h3] := ih (upren ξ).
    split=> *; rewrite /= !up_ren ?h1 ?h2 ?h3 //=.
    rewrite /rall closed_subst=>//.
    by apply closed_joker.
  - move=> B e ih ξ.
    have [h _ _] := ih ξ.
    have {}h p d : (VC p d (EBar B e)).[ren ξ] = VC p d (EBar B e).[ren ξ]
      by rewrite /= h.
    by split.
  - move=> e ih1 B π b ih2 ξ.
    have [h1 _ _] := ih1 (upren ξ).
    have [_ h2 h3] := ih2 (upren ξ).
    have h p d :
      (VC p d (EDef e B π b)).[ren ξ] = VC p d (EDef e B π b).[ren ξ].
    { rewrite /= !up_ren h1 h2 h3.
      rewrite /rlet closed_subst=>//.
      by apply closed_joker. }
    by split.
Qed.

Definition closing (Γ : ctx) (σ : var -> recipe) :=
  forall x, closed (σ x) /\ [ ⊢ σ x :- Γ x ].

Lemma closed_subst_closed r (σ : var -> recipe) :
  (forall x, closed (σ x)) ->
  closed r.[σ].
Proof.
  move=> hσ.
  rewrite /closed /fv upn0 subst_comp.
  f_equal.
  f_ext=> x /=.
  have := hσ x.
  by rewrite /closed /fv upn0.
Qed.

Lemma closing_hsubst Γ σ θ :
  closing Γ σ -> closing Γ (σ >>| θ).
Proof.
  move=> hσ x.
  have [hc ht] := hσ x.
  split.
  - by apply closed_unaffectedh.
  - by apply has_type_hsubst_0.
Qed.

Lemma closing_box Γ σ t U :
  closed t -> [ ⊢ t :- U ] ->
  closing Γ σ -> closing (U .: Γ) (Box t .: σ).
Proof.
  move=> ??? [] * //=.
  split.
  - by apply closed_box.
  - by constructor.
Qed.

Corollary has_type_closing r Γ U σ a :
  [ Γ, a, a ⊢ r :- U ] ->
  closing Γ σ ->
  closed r.[σ] /\ [ ⊢ r.[σ] :- U ].
Proof.
  move=> /has_type_lower_0 ? hσ.
  split.
  - apply closed_subst_closed=> x.
    by have [??] := hσ x.
  - apply has_type_subst with Γ=>// x.
    by have [??] := hσ x.
Qed.

Lemma has_type_inst r Γ U θ σ a :
  [ Γ, a, a ⊢ r :- U ] ->
  closing Γ σ ->
  closed r.|[θ].[σ] /\ [ ⊢ r.|[θ].[σ] :- U ].
Proof.
  move=> /has_type_lower_0 *.
  apply has_type_closing with Γ 0=>//.
  have := has_type_hsubst_upn.
  by apply.
Qed.

Corollary has_type_inst_neu r Γ U θ σ a :
  [ Γ, a, a ⊢ r :- U ] ->
  closing Γ σ ->
  closed (neu r.|[θ].[σ]) /\ [ ⊢ neu r.|[θ].[σ] :- U ].
Proof.
  move=> hr hσ.
  have [??] := has_type_inst θ hr hσ.
  split.
  - by apply closed_sneu.
  - by apply has_type_neu.
Qed.

Definition uniformly P Γ (r : recipe) : Prop :=
  forall σ θ, closing Γ σ ->
  P r.|[θ].[σ] /\ P (neu r).|[θ].[σ].

Definition uniformly2 P Γ (r s : recipe) : Prop :=
  forall σ θ, closing Γ σ ->
  P r.|[θ].[σ] s.|[θ].[σ] /\ P (neu r).|[θ].[σ] (neu s).|[θ].[σ].

Definition uniformly3 P Γ (r s t : recipe) : Prop :=
  forall σ θ, closing Γ σ ->
  P r.|[θ].[σ] s.|[θ].[σ] t.|[θ].[σ] /\
  P (neu r).|[θ].[σ] (neu s).|[θ].[σ] (neu t).|[θ].[σ].

Definition UNEU U := uniformly (NEU U).

Lemma UNEU_neu Γ U r a :
  [ Γ, a, a ⊢ r :- U ] ->
  UNEU U Γ (Neu r).
Proof.
  move=> /has_type_lower_0 hr ? θ hσ.
  have [??] := has_type_inst θ hr hσ.
  have [??] := has_type_inst θ (has_type_neu hr) hσ.
  by split; apply NEU_Neu.
Qed.

Lemma UNEU_and Γ U r s a :
  [ Γ, a, a ⊢ r :- U ] ->
  [ Γ, a, a ⊢ s :- U ] ->
  UNEU U Γ r ->
  UNEU U Γ s ->
  UNEU U Γ (And r s).
Proof.
  move=> /has_type_lower_0 hr
         /has_type_lower_0 hs.
  move=> ++ ? θ hσ => /(_ _ θ hσ) [??]
                   => /(_ _ θ hσ) [??].
  have [??] := has_type_inst θ hr hσ.
  have [??] := has_type_inst θ hs hσ.
  have [??] := has_type_inst θ (has_type_neu hr) hσ.
  have [??] := has_type_inst θ (has_type_neu hs) hσ.
  by split; apply NEU_and.
Qed.

Lemma UNEU_app Γ U V r s a :
  [ Γ, a, a ⊢ s :- U ] ->
  UNEU (Arr U V) Γ r ->
  UNEU U Γ s ->
  UNEU V Γ (App r s).
Proof.
  move=> /has_type_lower_0 ? + us σ θ hσ => /(_ _ θ hσ) [??].
  have happ u t :
    NEU (Arr U V) u.|[θ].[σ] ->
    [ Γ, 0, 0 ⊢ t :- U ] ->
    (forall σ θ, closing Γ σ -> NEU U t.|[θ].[σ]) ->
    NEU V (App u t).|[θ].[σ].
  { move=> hr ht hn.
    have [??] := has_type_inst θ ht hσ.
    apply hr=>// ξ.
    asimpl.
    have h: closing Γ (σ >>| ren ξ) by apply closing_hsubst.
    have [??] := has_type_inst (θ >> ren ξ) ht h.
    split.
    - by apply hn.
    - by apply neuneug. }
  split.
  - apply happ=>// σ' θ' h.
    by apply (us σ' θ' h).
  - apply happ=>//.
    + by apply has_type_neu.
    + move=> σ' θ' h.
      by apply (us σ' θ' h).
Qed.

Lemma UNEU_tlam Γ U r a :
  [ Γ, a.+1, a.+1 ⊢ r :- U ] ->
  UNEU U Γ r ->
  UNEU (TArr U) Γ (TLam r).
Proof.
  move=> /has_type_lower_n1 ? ur σ θ hσ.
  have htlam s :
    [ Γ, 1, 1 ⊢ s :- U ] ->
    (forall θ, NEU U s.|[θ].[σ]) ->
    NEU (TArr U) (TLam s).|[θ].[σ].
  { move=> hr' *.
    have [??] := has_type_inst θ (ty_tlam hr') hσ.
    apply NEU_tlam=>// *.
    by autosubst. }
  split.
  - apply htlam=>// τ.
    by apply (ur σ τ hσ).
  - apply htlam.
    + by apply has_type_neu.
    + move=> τ. by apply (ur σ τ hσ).
Qed.

Lemma UNEU_lam Γ U V r a :
  [ U .: Γ, a, a ⊢ r :- V ] ->
  UNEU V (U .: Γ) r ->
  UNEU (Arr U V) Γ (Lam r U).
Proof.
  move=> /has_type_lower_0 ? ur σ θ hσ.
  have hlam s :
    [ U .: Γ, 0, 0 ⊢ s :- V ] ->
    (forall σ, closing (U .: Γ) σ -> NEU V s.|[θ].[σ]) ->
    NEU (Arr U V) (Lam s U).|[θ].[σ].
  { move=> hr' hn.
    have [??] := has_type_inst θ (ty_lam hr') hσ.
    apply NEU_lam=>// *.
    asimpl.
    by apply hn, closing_box. }
  split.
  - apply hlam=>// σ' h.
    by apply (ur σ' θ h).
  - apply hlam.
    + by apply has_type_neu.
    + move=> σ' h.
      by apply (ur σ' θ h).
Qed.

Lemma UNEU_beta Γ U V r s a :
  [ U .: Γ, a, a ⊢ r :- V ] ->
  [ Γ, a, a ⊢ s :- U ] ->
  UNEU V (U .: Γ) r ->
  UNEU V Γ (App (Lam r U) s).
Proof.
  move=> /has_type_lower_0 ? /has_type_lower_0 ? ur σ θ hσ.
  have hbeta u t :
    [ U .: Γ, 0, 0 ⊢ u :- V ] ->
    [ Γ, 0, 0 ⊢ t :- U ] ->
    (forall σ, closing (U .: Γ) σ -> NEU V u.|[θ].[σ]) ->
    NEU V (App (Lam u U) t).|[θ].[σ].
  { move=> hr' hs' hn.
    have [??] := has_type_inst θ hs' hσ.
    have [??] := has_type_inst θ (ty_lam hr') hσ.
    apply NEU_beta=>//.
    asimpl.
    by apply hn, closing_box. }
  split.
  - apply hbeta=>// σ' h.
    by apply (ur σ' θ h).
  - apply hbeta.
    + by apply has_type_neu.
    + by apply has_type_neu.
    + move=> σ' h.
      by apply (ur σ' θ h).
Qed.

Lemma VC_neutral Γ e π :
  [ Γ ⊩ e :- π ] -> UNEU π Γ (VC false false e).
Proof.
  have:
    (forall Γ e π, [ Γ ⊩ e :- π ] -> UNEU π Γ (VC false false e)) /\
    (forall Γ π b, [ Γ ⊩ π ↦ b ] -> UNEU Void Γ (all_params (VC false false) b)).
  2: { by move=> [] + _; apply. }
  (* prove the generalization *)
  clear_all.
  apply cty_cabs_mut.
  { move=> > <-.
    apply UNEU_neu with 0.
    by constructor. }
  { move=> > _ ih σ θ hσ.
    have [h1 h2] := ih σ θ hσ.
    by split; [apply h1|apply h2]. }
  { move=> ??? U *.
    apply UNEU_app with U 0=>//.
    by apply ty_VC. }
  { move=> *.
    apply UNEU_tlam with 0=>//=.
    by apply ty_VC. }
  { move=> > he ?.
    have ? := ty_VC false false 0 he. (*bb*)
    have ? := ty_VC true true 0 he. (*tt*)
    apply UNEU_and with 0; try by (repeat constructor).
    + by apply UNEU_lam with 0.
    + apply UNEU_neu with 0.
      by constructor. }
  { by move=> ? [] *. }
  { move=> ??? U ? he ? hb ? /=.
    rewrite sel_eq.
    have ? := ty_VC false false 0 he.
    have [??] := ty_params true false 0 hb.
    have [??] := ty_params false false 0 hb.
    apply UNEU_beta with 0.
    + by constructor.
    + apply ty_app with U.
      * by constructor.
      * by apply has_type_joker_gen=> *; constructor.
    + by apply UNEU_and with 0. }
  { by move=> ? [] > hb * //; inv hb. }
  { move=> Γ ??? + /= σ θ hσ.
    have h : closing Γ (σ >>| ren (+1)) by apply closing_hsubst.
    move=> /(_ _ (up θ) h) [??].
    by split; apply NEU_tall. }
  { move=> > hb *.
    have [??] := ty_params false false 0 hb.
    apply UNEU_beta with 0=>//.
    apply has_type_joker_gen=> *.
    - by constructor.
    - by constructor. }
Qed.

Definition weakly_uniform2 P Γ (r s : recipe) : Prop :=
  forall σ θ, closing Γ σ ->
  P (neu r.|[θ].[σ]) (neu s.|[θ].[σ]).

Definition UEQU U := uniformly2 (EQU U).
Definition WUEQU U := weakly_uniform2 (EQU U).

Lemma WUEQU_app Γ U V r1 r2 s1 s2 a :
  [ Γ, a, a ⊢ s1 :- U ] ->
  [ Γ, a, a ⊢ s2 :- U ] ->
  WUEQU (Arr U V) Γ r1 r2 ->
  WUEQU U Γ s1 s2 ->
  WUEQU V Γ (App r1 s1) (App r2 s2).
Proof.
  move=> h1 h2 ur us σ θ hσ /=.
  have [??] := has_type_inst_neu θ h1 hσ.
  have [??] := has_type_inst_neu θ h2 hσ.
  have hs ξ :
    strongly2 (EQU U) (neu s1.|[θ].[σ]).|[ren ξ] (neu s2.|[θ].[σ]).|[ren ξ].
  { have h : closing Γ (σ >>| ren ξ) by apply closing_hsubst.
    rewrite /strongly2 -!neu_hsubst_comm !neu_idempotent.
    asimpl.
    by split; apply us. }
  have [e1 e2] := ur σ θ hσ.
  split.
  - apply e1=>// ξ.
    by have [[??] [??]] := hs ξ.
  - apply e2=>// ξ.
    by have [[??] [??]] := hs ξ.
Qed.

Lemma WUEQU_and_comm Γ U r s a :
  [ Γ, a, a ⊢ r :- U ] ->
  [ Γ, a, a ⊢ s :- U ] ->
  WUEQU U Γ (And r (Neu s)) (And s (Neu r)).
Proof.
  move=> hr hs ? θ hσ /=.
  have [??] := has_type_inst_neu θ hr hσ.
  have [??] := has_type_inst_neu θ hs hσ.
  apply EQU_and_comm=>//; by rewrite neu_idempotent.
Qed.

Lemma WUEQU_tlam Γ U r1 r2 a :
  [ Γ, a.+1, a.+1 ⊢ r1 :- U ] ->
  [ Γ, a.+1, a.+1 ⊢ r2 :- U ] ->
  WUEQU U Γ r1 r2 ->
  WUEQU (TArr U) Γ (TLam r1) (TLam r2).
Proof.
  move=> h1 h2 ur σ θ hσ /=.
  have [??] := has_type_inst_neu θ (ty_tlam h1) hσ.
  have [??] := has_type_inst_neu θ (ty_tlam h2) hσ.
  apply EQU_tlam=>// T.
  rewrite -!neu_hsubst_comm.
  asimpl.
  by apply ur.
Qed.

(* For any expression e, the recipe Cpd(e) is uniformly weakly equivalent to Cnpnd(e) *)
Lemma VC_notnot Γ e π p d :
  [ Γ ⊩ e :- π ] ->
  WUEQU π Γ (VC p d e) (VC (~~ p) (~~ d) e).
Proof with by auto using ty_VC.
  move=> h. move: Γ e π h p d.
  apply (cty_mut (P := fun Γ e π _ => forall p d, WUEQU π Γ (VC p d e) (VC (~~ p) (~~ d) e))
                 (P0 := fun _ _ _ _ => True))=> //.
  - move=> Γ h π <- p d σ θ hσ.
    have [hc ht] := hσ h.
    have [??] := EQU_neuneuneu hc ht.
    by case: p=> /=; split.
  - move=> > _ + p d σ θ hσ /= => /(_ p d σ θ hσ) [] h1 h2.
    by split; [apply h1|apply h2].
  - move=> ??? U ? ? ih1 ? ih2 >.
    apply WUEQU_app with U 0...
  - move=> *. apply WUEQU_tlam with 0...
  - move=> > ???? /=.
    rewrite !negbK.
    apply WUEQU_and_comm with 0; constructor...
  - by move=> ? [] * /=; auto.
  - move=> Γ e I π b ???? p d σ θ hσ.
    have h : [ Γ ⊩ EDef e I π b :- Void ] by constructor.
    have [??] := has_type_inst θ (ty_VC p d 0 h) hσ.
    have [??] := has_type_inst θ (ty_VC (~~ p) (~~ d) 0 h) hσ.
    by apply EQU_Void_neu.
Qed.

Definition UMEET U := uniformly3 (MEET U).

Lemma VC_split Γ e π p d:
  [ Γ ⊩ e :- π ] ->
  UEQU π Γ (VC true true e) (And (VC p d e) (VC (~~ p) (~~ d) e)).
Proof.
  move=> h. move: Γ e π h p d.
  apply (cty_mut (P := fun Γ e π _ => forall p d,
                          UEQU π Γ (VC true true e)
                                   (And (VC p d e) (VC (~~ p) (~~ d) e)))
                 (P0 := fun _ _ _ _ => True))=> //.
  - move=> ? x π <- p > hσ.
    have [hc ht] := hσ x.
    have ? := EQU_and_Neu1 hc ht.
    have ? := EQU_and_Neu2 hc ht.
    by case: p=> /=; split.
  - admit.
  - admit.
  - admit.
  - admit.
  - by move=> ? [] > ? ih ?? /=; apply ih.
  - admit.
Admitted.

(* For any expression e, the recipe Ctt(e) is a uniform meet of Cpd(e) and Cnpnd(e). *)
Lemma VC_meet Γ e π p d:
  [ Γ ⊩ e :- π ] ->
  UMEET π Γ (VC true true e) (VC p d e) (VC (~~ p) (~~ d) e).
Proof.
  move=> he σ θ hσ.
  have [??] := has_type_inst θ (ty_VC true true 0 he) hσ.
  have [??] := has_type_inst θ (ty_VC p d 0 he) hσ.
  have [??] := has_type_inst θ (ty_VC (~~ p) (~~ d) 0 he) hσ.
  have [??] := has_type_inst θ (has_type_neu (ty_VC true true 0 he)) hσ.
  have [??] := has_type_inst θ (has_type_neu (ty_VC p d 0 he)) hσ.
  have [??] := has_type_inst θ (has_type_neu (ty_VC (~~ p) (~~ d) 0 he)) hσ.
  have [e1 e2] := VC_split p d he θ hσ.
  have hw := VC_notnot p d he θ hσ.
  split.
  - apply l_3_10=>//.
  - apply l_3_10=>//.
    split=>//.
    by rewrite -!neu_hsubst_comm !neu_subst_neu.
Qed.

(* For any expression of the form g:ρ->e, the recipe Ctt(g:ρ->e) is uniformly equivalent to λg:ρ.Ctt(e) *)