DecSyn.logrel

Logical predicate and "semantic" soundness

We use a logical predicate to prove strong normalization for well-typed terms. While the fundamental theorem is often referred to as semantic soundness, our modeling of conversion as untyped subtyping is not quite as semantic as it normally is.

Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax.
Require Import common fp_red.
From Hammer Require Import Tactics.
Require Import ssreflect ssrbool.
From stdpp Require Import relations (rtc(..), rtc_subrel).
Import Psatz.

Function space
Definition ProdSpace (PA : PTm Prop)
  (PF : PTm (PTm Prop) Prop) b : Prop :=
   a PB, PA a PF a PB PB (PApp b a).

Dependent pair space
Definition SumSpace (PA : PTm Prop)
  (PF : PTm (PTm Prop) Prop) t : Prop :=
  ( v, rtc TRedSN t v SNe v) a b, rtc TRedSN t (PPair a b) PA a ( PB, PF a PB PB b).

Inspired by Girard's reduciblity candidates
Definition CR (P : PTm Prop) :=
  ( a, P a SN a)
    ( a, SNe a P a).

Definition BindSpace p := if p is PPi then ProdSpace else SumSpace.

An equivalence relation between predicates on terms/subsets of terms
Notation "S0 ≐ S1" := ( (A : PTm), A A) (at level 70, no associativity).

Lemma redsn_preservation_mutual :
  ( (a : PTm) (s : SNe a), b, TRedSN a b False)
    ( (a : PTm) (s : SN a), b, TRedSN a b SN b)
  ( (a b : PTm) (_ : TRedSN a b), c, TRedSN a c b = c).
Proof.
  apply sn_mutual; sauto lq:on rew:off.
Qed.

Lemma redsns_preservation : a b, SN a rtc TRedSN a b SN b.
Proof. induction 2; sfirstorder use:redsn_preservation_mutual ctrs:rtc. Qed.

#[export]Hint Resolve Sub.sne_bind_noconf Sub.sne_univ_noconf Sub.bind_univ_noconf
  Sub.bind_sne_noconf Sub.univ_sne_noconf Sub.univ_bind_noconf Sub.nat_bind_noconf Sub.bind_nat_noconf Sub.sne_nat_noconf Sub.nat_sne_noconf Sub.univ_nat_noconf Sub.nat_univ_noconf: noconf.

Make sure that the motive used in the induction principle of InterpUniv is oblivious of the syntactic differences between predicates.
Definition ind_motive_okay (P : PTm (PTm Prop) Prop) :=
   i A S S', S ≐ S' P i A S P i A S'.

The declarative signature of the logical predicate

Since the logical predicate can't be defined directly, we first specify a clean interface for its introduction rules and induction principle.
Module Type LogRel.

The logical predicate

  Parameter InterpUniv : PTm (PTm Prop) Prop.
  Notation "⟦ A ⟧ i ↘ S" := (InterpUniv i A S) (at level 70, no associativity).

Introduction rules

  Axiom InterpUniv_Ne : i (A : PTm),
    SNe A
    ⟦ A ⟧ i ↘ (fun a v, rtc TRedSN a v SNe v).

  Axiom InterpUniv_Bind : i p A B PA PF,
    ⟦ A ⟧ i ↘ PA
    ( a, PA a PB, PF a PB)
    ( a PB, PF a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
    ⟦ PBind p A B ⟧ i ↘ BindSpace p PA PF.

  Axiom InterpUniv_Univ : i j,
    j < i ⟦ PUniv j ⟧ i ↘ (fun A PA, ⟦ A ⟧ j ↘ PA).

  Axiom InterpUniv_Step : i A A0 PA,
    TRedSN A
    ⟦ ⟧ i ↘ PA
    ⟦ A ⟧ i ↘ PA.

  Axiom InterpUniv_Nat : i,
    ⟦ PNat ⟧ i ↘ SNat.

  Axiom InterpUniv_Conv : i A S S',
    ⟦ A ⟧ i ↘ S S ≐ S' ⟦ A ⟧ i ↘ S'.

Induction principles

  Axiom InterpUniv_ind
  : (P : PTm (PTm Prop) Prop),
       ind_motive_okay P
       ( i (A : PTm), SNe A P i A (fun a : PTm v : PTm , rtc TRedSN a v SNe v))
       ( i (p : BTag) (A : PTm ) (B : PTm ) (PA : PTm Prop)
          (PF : PTm (PTm Prop) Prop),
        ⟦ A ⟧ i ↘ PA
        P i A PA
        ( a : PTm , PA a PB : PTm Prop, PF a PB)
        ( (a : PTm ) (PB : PTm Prop), PF a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
        ( (a : PTm ) (PB : PTm Prop), PF a PB P i (subst_PTm (scons a VarPTm) B) PB)
        P i (PBind p A B) (BindSpace p PA PF))
       ( i, P i PNat SNat)
       ( i j : , j < i ( A PA, ⟦ A ⟧ j ↘ PA P j A PA) P i (PUniv j) (fun A PA, ⟦ A ⟧ j ↘ PA))
       ( i (A A0 : PTm ) (PA : PTm Prop), TRedSN A ⟦ ⟧ i ↘ PA P i PA P i A PA)
        i (p : PTm ) (P0 : PTm Prop), ⟦ p ⟧ i ↘ P i p .
  #[export]Hint Resolve InterpUniv_Bind InterpUniv_Step InterpUniv_Ne InterpUniv_Univ InterpUniv_Conv InterpUniv_Nat : InterpUniv.

End LogRel.

A signature containing the facts we'd like to derive from the logical predicate

Module Type LogRelFacts (M : LogRel).
  Import M.

  Axiom cumulative : i (A : PTm) PA,
      ⟦ A ⟧ i ↘ PA j, i j
                             ⟦ A ⟧ j ↘ PA.

  Axiom adequacy : i A PA,
      ⟦ A ⟧ i ↘ PA
      CR PA SN A.

  Axiom back_clos : i (A : PTm ) PA,
    ⟦ A ⟧ i ↘ PA
     a b, TRedSN a b
            PA b PA a.

  Axiom back_closs : i (A : PTm) PA,
    ⟦ A ⟧ i ↘ PA
     a b, rtc TRedSN a b
           PA b PA a.

  Axiom case : i (A : PTm) PA,
    ⟦ A ⟧ i ↘ PA
     H, rtc TRedSN A H ⟦ H ⟧ i ↘ PA (SNe H isbind H isuniv H isnat H).

  Axiom SNe_inv : i (A : PTm) PA,
    SNe A
    ⟦ A ⟧ i ↘ PA
    (PA ≐ (fun a v, rtc TRedSN a v SNe v)).

  Axiom Bind_inv : i p A B S,
    ⟦ PBind p A B ⟧ i ↘ S PA PF,
        ⟦ A ⟧ i ↘ PA
          ( a, PA a PB, PF a PB)
          ( a PB, PF a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
          S ≐ BindSpace p PA PF.

  Axiom Nat_inv : i S,
    ⟦ PNat ⟧ i ↘ S S ≐ SNat.

  Axiom Univ_inv : i j S,
    ⟦ PUniv j ⟧ i ↘ S
    S ≐ (fun A PA, ⟦ A ⟧ j ↘ PA) j < i.

  Axiom sub : i j (A B : PTm) PA PB,
    ⟦ A ⟧ i ↘ PA
    ⟦ B ⟧ j ↘ PB
    Sub.R A B x, PA x PB x.

  Axiom functional : i j A PA PB,
      ⟦ A ⟧ i ↘ PA
      ⟦ A ⟧ j ↘ PB
      PA ≐ PB.

  Axiom join : i j (A B : PTm) PA PB,
    ⟦ A ⟧ i ↘ PA
    ⟦ B ⟧ j ↘ PB
    DJoin.R A B
    PA ≐ PB.

  Axiom Bind_inv_nopf : i p A B P, ⟦PBind p A B ⟧ i ↘ P
     (PA : PTm Prop),
      ⟦ A ⟧ i ↘ PA
        ( a, PA a PB, ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
        P ≐ BindSpace p PA (fun a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB).

  Axiom Bind_nopf : p i (A : PTm) B PA,
    ⟦ A ⟧ i ↘ PA
    ( a, PA a PB, ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
    ⟦ PBind p A B ⟧ i ↘ (BindSpace p PA (fun a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)).

End LogRelFacts.

Proofs of the properties about the logical predicate from the abstract interface LogRel

Module LogRelFactsImpl (M : LogRel) : LogRelFacts M.

  Import M.

  Lemma cumulative i (A : PTm) PA :
    ⟦ A ⟧ i ↘ PA j, i j ⟦ A ⟧ j ↘ PA.
  Proof.
    move : i A PA. apply : InterpUniv_ind;
      hauto l:on solve+:(by lia) db:InterpUniv unfold:ind_motive_okay.
  Qed.

  Lemma N_Exps (a b : PTm) :
    rtc TRedSN a b
    SN b
    SN a.
  Proof.
    induction 1; eauto using N_Exp.
  Qed.

Artifact for not using funext
  Lemma CR_okay S0 S1 :
     ≐ CR CR .
  Proof.
    unfold CR. sfirstorder.
  Qed.

  Lemma CR_SNat : CR SNat.
  Proof.
    rewrite /CR.
    split.
    induction 1; hauto q:on ctrs:SN,SNe.
    hauto lq:on ctrs:SNat.
  Qed.

  Lemma adequacy : i A PA,
   ⟦ A ⟧ i ↘ PA
   CR PA SN A.
  Proof.
    apply : InterpUniv_ind.
    - sfirstorder use:CR_okay.
    - hauto l:on use:N_Exps ctrs:SN,SNe.
    - move i p A B PA PF hPA [ ] hTot hRes ihPF.
      set PBot := (VarPTm var_zero).
      have hb : PA PBot by hauto q:on ctrs:SNe.
      have hb' : SN PBot by hauto q:on ctrs:SN, SNe.
      rewrite /CR.
      repeat split.
      + case : p //=.
        * rewrite /ProdSpace.
          qauto use:SN_AppInv unfold:CR.
        * hauto q:on unfold:SumSpace use:N_SNe, N_Pair,N_Exps.
      + move a ha.
        case : p/=.
        * rewrite /ProdSpace *.
          suff : SNe (PApp a ) by sfirstorder.
          hauto q:on use:N_App.
        * sfirstorder.
      + apply N_Bind//=.
        have : SN (PApp (PAbs B) PBot).
        apply : N_Exp; eauto using N_β.
        hauto lq:on.
        qauto l:on use:SN_AppInv, SN_NoForbid.P_AbsInv.
    - sfirstorder use:CR_SNat.
    - hauto l:on db:InterpUniv.
    - hauto l:on ctrs:SN unfold:CR.
  Qed.

  Lemma back_clos i (A : PTm ) PA :
    ⟦ A ⟧ i ↘ PA
     a b, TRedSN a b
           PA b PA a.
  Proof.
    move : i A PA . apply : InterpUniv_ind; eauto.
    - hauto lq:on unfold:ind_motive_okay.
    - hauto q:on ctrs:rtc.
    - move i p A B PA PF hPA ihPA hTot hRes ihPF a b hr.
      case : p //=.
      + rewrite /ProdSpace.
        move hba PB ha hPB.
        suff : TRedSN (PApp a ) (PApp b ) by hauto lq:on.
        apply N_AppL //=.
        hauto q:on use:adequacy.
      + hauto lq:on ctrs:rtc unfold:SumSpace.
    - hauto lq:on ctrs:SNat.
    - hauto l:on use:InterpUniv_Step.
  Qed.

  Lemma back_closs i (A : PTm) PA :
    ⟦ A ⟧ i ↘ PA
     a b, rtc TRedSN a b
            PA b PA a.
  Proof.
    induction 2; hauto lq:on ctrs:rtc use:back_clos.
  Qed.

  Lemma case i (A : PTm) PA :
    ⟦ A ⟧ i ↘ PA
     H, rtc TRedSN A H ⟦ H ⟧ i ↘ PA (SNe H isbind H isuniv H isnat H).
  Proof.
    move : i A PA. apply InterpUniv_ind //=; sauto lq:on db:InterpUniv ctrs:rtc unfold:ind_motive_okay.
  Qed.

  Lemma SNe_inv i (A : PTm) PA :
    SNe A
    ⟦ A ⟧ i ↘ PA
    (PA ≐ (fun a v, rtc TRedSN a v SNe v)).
  Proof.
    move /[swap]. move : i A PA.
    apply : InterpUniv_ind; hauto lq:on use:redsn_preservation_mutual unfold:ind_motive_okay inv:SNe, TRedSN.
  Qed.

  Lemma Bind_inv i p A B S :
    ⟦ PBind p A B ⟧ i ↘ S PA PF,
        ⟦ A ⟧ i ↘ PA
          ( a, PA a PB, PF a PB)
          ( a PB, PF a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
          S ≐ BindSpace p PA PF.
  Proof.
    move E : (PBind p A B) T h. move : p A B E.
    elim /InterpUniv_ind : h; hauto lq:on unfold:ind_motive_okay inv:SNe, TRedSN.
  Qed.

  Lemma Nat_inv i S :
    ⟦ PNat ⟧ i ↘ S S ≐ SNat.
  Proof.
    move E : (PNat) T hu. move : E.
    elim /InterpUniv_ind : hu; hauto lq:on unfold:ind_motive_okay inv:SNe, TRedSN.
  Qed.

  Lemma Univ_inv i j S :
    ⟦ PUniv j ⟧ i ↘ S
    S ≐ (fun A PA, ⟦ A ⟧ j ↘ PA) j < i.
  Proof.
    move E : (PUniv j) T h. move : j E.
    elim /InterpUniv_ind : h; hauto lq:on unfold:ind_motive_okay inv:SNe, TRedSN.
  Qed.

  Lemma bindspace_impl p (PA PA0 : PTm Prop) PF PF0 b :
    ( x, if p is PPi then ( x PA x) else (PA x x))
    ( (a : PTm ) (PB PB0 : PTm Prop), a PF a PB a ( x, PB x x))
    ( a, PA a PB, PF a PB)
    ( a, a PB0, a )
    (BindSpace p PA PF b BindSpace p b).
  Proof.
    rewrite /BindSpace hSA h hPF .
    case : p hSA /= hSA.
    - rewrite /ProdSpace.
      move a PB ha hPF'.
      have {}/hPF : PA a by sfirstorder.
      specialize with (1 := ha).
      hauto lq:on.
    - rewrite /SumSpace.
      case. sfirstorder.
      move [][][][]. right.
      hauto lq:on.
  Qed.

  Lemma sub' i (A B : PTm) PA PB :
    ⟦ A ⟧ i ↘ PA
    ⟦ B ⟧ i ↘ PB
    ((Sub.R A B x, PA x PB x)
       (Sub.R B A x, PB x PA x)).
  Proof.
    move hA.
    move : i A PA hA B PB.
    apply : InterpUniv_ind.
    - hauto lq:on unfold:ind_motive_okay.
    - move i A hA B PB hPB. split.
      + move hAB a ha.
        have [? ?] : SN B SN A by hauto l:on use:adequacy.
        move /case : hPB.
        move [H [/DJoin.FromRedSNs h [ ]]].
        have {h}{}hAB : Sub.R A H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
        have {} : SNe H.
        suff : isbind H isuniv H isnat H by sfirstorder b:on.
        move : hA hAB. clear. hauto lq:on db:noconf.
        eapply SNe_inv in ;
          qauto l:on.
      + move hAB a ha.
        have [? ?] : SN B SN A by hauto l:on use:adequacy.
        move /case : hPB.
        move [H [/DJoin.FromRedSNs h [ ]]].
        have {h}{}hAB : Sub.R H A by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
        have {} : SNe H.
        suff : isbind H isuniv H isnat H by sfirstorder b:on.
        move : hAB hA . clear. hauto lq:on db:noconf.
        eapply SNe_inv in ;
          qauto l:on.
    - move i p A B PA PF hPA ihPA hTot hRes ihPF U PU hU. split.
      + have hU' : SN U by hauto l:on use:adequacy.
        move /case : hU [H [/DJoin.FromRedSNs h [ ]]] hU.
        have {hU} {}h : Sub.R (PBind p A B) H
          by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
        have{} : isbind H.
        suff : SNe H isuniv H isnat H by sfirstorder b:on.
        have : isbind (PBind p A B) by scongruence.
        move : h. clear. hauto l:on db:noconf.
        case : H h //=.
        move /Sub.bind_inj.
        move [? [hA hB]] _. subst.
        move /Bind_inv : .
        move [][][][][ h]. setoid_rewrite h. move {PU h}.
        move x. apply bindspace_impl; eauto;[idtac|idtac]. hauto l:on.
        move a PB PB' ha hPB hPB'.
        move : hPB'. repeat move/[apply].
        move : ihPF hPB. repeat move/[apply].
        move h. eapply h.
        apply Sub.cong //=; eauto using DJoin.refl.
      + have hU' : SN U by hauto l:on use:adequacy.
        move /case : hU [H [/DJoin.FromRedSNs h [ ]]] hU.
        have {hU} {}h : Sub.R H (PBind p A B)
          by move : hU hU' h; clear; hauto q:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
        have{} : isbind H.
        suff : SNe H isuniv H isnat H by sfirstorder b:on.
        have : isbind (PBind p A B) by scongruence.
        move : h. clear. move : (PBind p A B). hauto lq:on db:noconf.
        case : H h //=.
        move /Sub.bind_inj.
        move [? [hA hB]] _. subst.
        move /Bind_inv : .
        move [][][][][ h]. setoid_rewrite h {PU h}.
        move x. apply bindspace_impl; eauto;[idtac|idtac]. hauto l:on.
        move a PB PB' ha hPB hPB'.
        eapply ihPF; eauto.
        apply Sub.cong //=; eauto using DJoin.refl.
    - move i B PB h. split.
      + move hAB a ha.
        have ? : SN B by hauto l:on use:adequacy.
        move /case : h.
        move [H [/DJoin.FromRedSNs h [ ]]].
        have {h}{}hAB : Sub.R PNat H by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
        have {} : isnat H.
        suff : isbind H isuniv H SNe H by sfirstorder b:on.
        have : @isnat PNat by simpl.
        move : hAB. clear. qauto l:on db:noconf.
        case : H hAB //=.
        hauto lq:on use:Nat_inv.
      + move hAB a ha.
        have ? : SN B by hauto l:on use:adequacy.
        move /case : h.
        move [H [/DJoin.FromRedSNs h [ ]]].
        have {h}{}hAB : Sub.R H PNat by qauto l:on use:Sub.FromJoin, DJoin.symmetric, Sub.transitive.
        have {} : isnat H.
        suff : isbind H isuniv H SNe H by sfirstorder b:on.
        have : @isnat PNat by simpl.
        move : hAB. clear. qauto l:on db:noconf.
        case : H hAB //=.
        hauto lq:on use:Nat_inv.
    - move i j jlti ih B PB hPB. split.
      + have ? : SN B by hauto l:on use:adequacy.
        move /case : hPB [H [/DJoin.FromRedSNs h [ ]]].
        move hj.
        have {hj}{}h : Sub.R (PUniv j) H by eauto using Sub.transitive, Sub.FromJoin.
        have {} : isuniv H.
        suff : SNe H isbind H isnat H by tauto. move : h. clear. hauto lq:on db:noconf.
        case : H h //=.
        move j' hPB h _.
        have {}h : j j' by hauto lq:on use: Sub.univ_inj. subst.
        move /Univ_inv : hPB [? ?]. subst.
        have ? : j i by lia.
        move A. hauto l:on use:cumulative.
      + have ? : SN B by hauto l:on use:adequacy.
        move /case : hPB [H [/DJoin.FromRedSNs h [ ]]].
        move hj.
        have {hj}{}h : Sub.R H (PUniv j) by eauto using Sub.transitive, Sub.FromJoin, DJoin.symmetric.
        have {} : isuniv H.
        suff : SNe H isbind H isnat H by tauto. move : h. clear. hauto lq:on db:noconf.
        case : H h //=.
        move j' hPB h _.
        have {}h : j' j by hauto lq:on use: Sub.univ_inj.
        move /Univ_inv : hPB [? ?]. subst.
        move A. hauto l:on use:cumulative.
    - move i A PA hr hPA ihPA B PB hPB.
      have ? : SN A by sauto lq:on use:adequacy.
      split.
      + move ?.
        have {}hr : Sub.R A by hauto lq:on ctrs:rtc use:DJoin.FromRedSNs, DJoin.symmetric, Sub.FromJoin.
        have : Sub.R B by eauto using Sub.transitive.
        qauto l:on.
      + move ?.
        have {}hr : Sub.R A by hauto lq:on ctrs:rtc use:DJoin.FromRedSNs, DJoin.symmetric, Sub.FromJoin.
        have : Sub.R B by eauto using Sub.transitive.
        qauto l:on.
  Qed.

  Lemma sub0 i (A B : PTm) PA PB :
    ⟦ A ⟧ i ↘ PA
    ⟦ B ⟧ i ↘ PB
    Sub.R A B x, PA x PB x.
  Proof.
    move : sub'. repeat move/[apply].
    move [+ _]. apply.
  Qed.

  Lemma sub i j (A B : PTm) PA PB :
    ⟦ A ⟧ i ↘ PA
    ⟦ B ⟧ j ↘ PB
    Sub.R A B x, PA x PB x.
  Proof.
    have [? ?] : i max i j j max i j by lia.
    move hPA hPB.
    have : ⟦ B ⟧ (max i j) ↘ PB by eauto using cumulative.
    have : ⟦ A ⟧ (max i j) ↘ PA by eauto using cumulative.
    move : sub0. repeat move/[apply].
    apply.
  Qed.

  Lemma InterpUniv_Join i (A B : PTm) PA PB :
    ⟦ A ⟧ i ↘ PA
    ⟦ B ⟧ i ↘ PB
    DJoin.R A B
    PA ≐ PB.
  Proof.
    move + + /[dup] /Sub.FromJoin + /DJoin.symmetric /Sub.FromJoin.
    move : sub'; repeat move/[apply]. hauto l:on.
  Qed.

  Lemma InterpUniv_Functional i (A : PTm) PA PB :
    ⟦ A ⟧ i ↘ PA
    ⟦ A ⟧ i ↘ PB
    PA ≐ PB.
  Proof. hauto l:on use:InterpUniv_Join, DJoin.refl. Qed.

  Lemma join i j (A B : PTm) PA PB :
    ⟦ A ⟧ i ↘ PA
    ⟦ B ⟧ j ↘ PB
    DJoin.R A B
    PA ≐ PB.
  Proof.
    have [? ?] : i max i j j max i j by lia.
    move hPA hPB.
    have : ⟦ A ⟧ (max i j) ↘ PA by eauto using cumulative.
    have : ⟦ B ⟧ (max i j) ↘ PB by eauto using cumulative.
    eauto using InterpUniv_Join.
  Qed.

  Lemma functional i j A PA PB :
    ⟦ A ⟧ i ↘ PA
    ⟦ A ⟧ j ↘ PB
    PA ≐ PB.
  Proof.
    hauto l:on use:join, DJoin.refl.
  Qed.

  Lemma Bind_inv_nopf i p A B P (h : ⟦PBind p A B ⟧ i ↘ P) :
     (PA : PTm Prop),
      ⟦ A ⟧ i ↘ PA
        ( a, PA a PB, ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
        P ≐ BindSpace p PA (fun a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB).
  Proof.
    move /Bind_inv : h.
    move [PA][PF][hPA][hPF][hPF']h. setoid_rewrite h {P h}.
    exists PA. split //.
    case : p /=.
    - split.
      hauto lq:on.
      split.
      + move h a PB ha.
        have {}/hPF := ha.
        move [ ].
        have {}/hPF' := ? ?.
        have : PB ≐ by eauto using functional.
        firstorder.
      + sfirstorder.
    - split.
      hauto lq:on.
      rewrite /SumSpace.
      move .
      split.
      + case; first by tauto.
        move [a][b][][]. right.
        exists a,b.
        repeat split //.
        move PB.
        have {}/hPF := .
        move []/[dup]?/hPF' .
        have h : PB ≐ by eauto using InterpUniv_Functional.
        setoid_rewrite h.
        firstorder.
      + case; first by tauto.
        move [a][b][][]. right.
        exists a,b.
        repeat split //.
        move PB.
        have {}/hPF := .
        move []/[dup]?/hPF' .
        have h : PB ≐ by eauto using InterpUniv_Functional.
        setoid_rewrite h.
        firstorder.
  Qed.

  Lemma Bind_nopf p i (A : PTm) B PA :
    ⟦ A ⟧ i ↘ PA
    ( a, PA a PB, ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
    ⟦ PBind p A B ⟧ i ↘ (BindSpace p PA (fun a PB => ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)).
  Proof.
    move => . apply InterpUniv_Bind => //=.
  Qed.

End LogRelFactsImpl.

An implementation of the LogRel signature with an explicit recursor InterpExt

Module LogRelImpl : LogRel.
  Reserved Notation "⟦ A ⟧ i ;; I ↘ S" (at level 70).

  Inductive InterpExt i (I : PTm Prop) : PTm (PTm Prop) Prop :=
  | InterpExt_Ne A :
    SNe A
    ⟦ A ⟧ i ;; I ↘ (fun a v, rtc TRedSN a v SNe v)

  | InterpExt_Bind p A B PA PF :
    ⟦ A ⟧ i ;; I ↘ PA
    ( a, PA a PB, PF a PB)
    ( a PB, PF a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ;; I ↘ PB)
    ⟦ PBind p A B ⟧ i ;; I ↘ BindSpace p PA PF

  | InterpExt_Nat :
    ⟦ PNat ⟧ i ;; I ↘ SNat

  | InterpExt_Univ j :
    j < i
    ⟦ PUniv j ⟧ i ;; I ↘ (I j)

  | InterpExt_Step A A0 PA :
    TRedSN A
    ⟦ ⟧ i ;; I ↘ PA
    ⟦ A ⟧ i ;; I ↘ PA

  
InterpExt_Conv's sole purpose is to get rid of funext and propext
  | InterpExt_Conv A PA PA' :
    ⟦ A ⟧ i ;; I ↘ PA
    PA ≐ PA'
    ⟦ A ⟧ i ;; I ↘ PA'
  where "⟦ A ⟧ i ;; I ↘ S" := (InterpExt i I A S).

  Lemma InterpExt_Univ' i I j (PF : PTm Prop) :
    PF = I j
    j < i
    ⟦ PUniv j ⟧ i ;; I ↘ PF.
  Proof. hauto lq:on ctrs:InterpExt. Qed.

  Infix "<?" := Compare_dec.lt_dec (at level 60).

Migrated from Equations to explicit recursion over Acc using Leroy's method: https://inria.hal.science/hal-04356563v2/document
  Fixpoint InterpUniv_rec (i : ) (ACC : Acc lt i) : PTm (PTm Prop) Prop :=
    @InterpExt i (fun j A
                    match j <? i with
                    | left h PA, InterpUniv_rec j (Acc_inv ACC h) A PA
                    | right _ False
                    end).

  Definition InterpUniv (i : ) : PTm (PTm Prop) Prop :=
    InterpUniv_rec i (Wf_nat.lt_wf i).

  Lemma InterpExt_lt_impl i I I' A (PA : PTm Prop) :
    ( j, j < i I j ≐ I' j)
    ⟦ A ⟧ i ;; I ↘ PA
    ⟦ A ⟧ i ;; I' ↘ PA.
  Proof.
    move hI h.
    elim : A PA /h.
    - hauto q:on ctrs:InterpExt.
    - hauto lq:on rew:off ctrs:InterpExt.
    - hauto q:on ctrs:InterpExt.
    - hauto q:on ctrs:InterpExt.
    - hauto lq:on ctrs:InterpExt.
    - hauto lq:on ctrs:InterpExt.
  Qed.

  Lemma InterpExt_lt_eq i I I' A (PA : PTm Prop) :
    ( j, j < i I j ≐ I' j)
    ⟦ A ⟧ i ;; I ↘ PA
      ⟦ A ⟧ i ;; I' ↘ PA.
  Proof.
    hfcrush use:InterpExt_lt_impl.
  Qed.

  Notation "⟦ A ⟧ i ↘ S" := (InterpUniv i A S) (at level 70, no associativity).

  Lemma InterpUniv_rec_acc_irrel i ACC ACC' A S :
    InterpUniv_rec i ACC A S InterpUniv_rec i ACC' A S.
  Proof.
    move : i ACC ACC' A S.
    elim /Wf_nat.lt_wf_ind.
    move n h [] [] A S /=.
    apply InterpExt_lt_eq.
    move j hj .
    case : (j <? n) //.
    hauto l:on.
  Qed.

  Lemma InterpUniv_rec_nolt i ACC A S :
    InterpUniv_rec i ACC A S InterpExt i (fun j (A : PTm ) PA, ⟦ A ⟧ j ↘ PA) A S.
  Proof.
    move : i ACC A S.
    elim /Wf_nat.lt_wf_ind.
    set (I := fun _ _).
    move n ih.
    case hAcc A S /=.
    apply InterpExt_lt_eq.
    move j h .
    case : (j <? n) //.
    hauto l:on use:InterpUniv_rec_acc_irrel unfold:InterpUniv.
  Qed.

  Lemma InterpUniv_nolt i A S :
    InterpUniv i A S InterpExt i (fun j (A : PTm ) PA, ⟦ A ⟧ j ↘ PA) A S.
  Proof. rewrite /InterpUniv; apply InterpUniv_rec_nolt. Qed.

  Lemma InterpUniv_ind
    : (P : PTm (PTm Prop) Prop),
      ind_motive_okay P
      ( i (A : PTm), SNe A P i A (fun a : PTm v : PTm , rtc TRedSN a v SNe v))
      ( i (p : BTag) (A : PTm ) (B : PTm ) (PA : PTm Prop)
          (PF : PTm (PTm Prop) Prop),
          ⟦ A ⟧ i ↘ PA
          P i A PA
          ( a : PTm , PA a PB : PTm Prop, PF a PB)
          ( (a : PTm ) (PB : PTm Prop), PF a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
          ( (a : PTm ) (PB : PTm Prop), PF a PB P i (subst_PTm (scons a VarPTm) B) PB)
          P i (PBind p A B) (BindSpace p PA PF))
      ( i, P i PNat SNat)
      ( i j : , j < i ( A PA, ⟦ A ⟧ j ↘ PA P j A PA) P i (PUniv j) (fun A PA, ⟦ A ⟧ j ↘ PA))
      ( i (A A0 : PTm ) (PA : PTm Prop), TRedSN A ⟦ ⟧ i ↘ PA P i PA P i A PA)
       i (p : PTm ) (P0 : PTm Prop), ⟦ p ⟧ i ↘ P i p .
  Proof.
    move P P_ok hSN hBind hNat hUniv hRed.
    elim /Wf_nat.lt_wf_ind i ih . setoid_rewrite InterpUniv_nolt.
    move A PA. move h. set I := fun _ _ in h.
    elim : A PA / h; eauto.
    - hauto l:on use:InterpUniv_nolt.
    - hauto l:on use:InterpUniv_nolt.
    - hauto lq:on unfold:ind_motive_okay.
  Qed.

  Lemma InterpUniv_Ne i (A : PTm) :
    SNe A
    ⟦ A ⟧ i ↘ (fun a v, rtc TRedSN a v SNe v).
  Proof. apply InterpExt_Ne. Qed.

  Lemma InterpUniv_Bind i p A B PA PF :
    ⟦ A ⟧ i ↘ PA
    ( a, PA a PB, PF a PB)
    ( a PB, PF a PB ⟦ subst_PTm (scons a VarPTm) B ⟧ i ↘ PB)
    ⟦ PBind p A B ⟧ i ↘ BindSpace p PA PF.
  Proof. apply InterpExt_Bind. Qed.

  Lemma InterpUniv_Univ i j :
    j < i ⟦ PUniv j ⟧ i ↘ (fun A PA, ⟦ A ⟧ j ↘ PA).
  Proof.
    setoid_rewrite InterpUniv_nolt. by apply InterpExt_Univ'.
  Qed.

  Lemma InterpUniv_Step i A A0 PA :
    TRedSN A
    ⟦ ⟧ i ↘ PA
    ⟦ A ⟧ i ↘ PA.
  Proof. apply InterpExt_Step. Qed.

  Lemma InterpUniv_Nat i :
    ⟦ PNat ⟧ i ↘ SNat.
  Proof. apply InterpExt_Nat. Qed.

  Lemma InterpUniv_Conv i A S S' :
    ⟦ A ⟧ i ↘ S S ≐ S' ⟦ A ⟧ i ↘ S'.
  Proof. apply InterpExt_Conv. Qed.
End LogRelImpl.

Instantiating LogRelFacts with the concrete implementation LogRelImpl

Now we have all the facts we need about the logical predicate without ever touching the messy definition in LogRelImpl!
Module LRFacts := LogRelFactsImpl LogRelImpl.
Import LogRelImpl.

Semantic typing defined in terms of the logical predicate

Definition ρ_ok (Γ : list PTm) (ρ : PTm) := i k A PA,
    lookup i Γ A
    ⟦ subst_PTm ρ A ⟧ k ↘ PA PA (ρ i).

Definition SemWt Γ (a A : PTm) := ρ, ρ_ok Γ ρ k PA, ⟦ subst_PTm ρ A ⟧ k ↘ PA PA (subst_PTm ρ a).
Notation "Γ ⊨ a ∈ A" := (SemWt Γ a A) (at level 70).

Definition SemEq Γ (a b A : PTm) := DJoin.R a b ρ, ρ_ok Γ ρ k PA, ⟦ subst_PTm ρ A ⟧ k ↘ PA PA (subst_PTm ρ a) PA (subst_PTm ρ b).
Notation "Γ ⊨ a ≡ b ∈ A" := (SemEq Γ a b A) (at level 70).

Definition SemLEq Γ (A B : PTm) := Sub.R A B i, ρ, ρ_ok Γ ρ S0 S1, ⟦ subst_PTm ρ A ⟧ i ↘ ⟦ subst_PTm ρ B ⟧ i ↘ .
Notation "Γ ⊨ a ≲ b" := (SemLEq Γ a b) (at level 70).

Lemma SemWt_Univ Γ (A : PTm) i :
  Γ ⊨ A ∈ PUniv i
   ρ, ρ_ok Γ ρ S, ⟦ subst_PTm ρ A ⟧ i ↘ S.
Proof.
  rewrite /SemWt.
  split.
  - hauto lq:on rew:off use:LRFacts.Univ_inv.
  - move /[swap] ρ /[apply].
    move [PA hPA].
    exists (S i). eexists.
    split.
    + hauto q:on db: InterpUniv.
    + simpl. eauto.
Qed.

Lemma SemEq_SemWt Γ (a b A : PTm) : Γ ⊨ a ≡ b ∈ A Γ ⊨ a ∈ A Γ ⊨ b ∈ A DJoin.R a b.
Proof. hauto lq:on rew:off unfold:SemEq, SemWt. Qed.

Lemma SemLEq_SemWt Γ (A B : PTm) : Γ ⊨ A ≲ B Sub.R A B i, Γ ⊨ A ∈ PUniv i Γ ⊨ B ∈ PUniv i.
Proof. hauto q:on use:SemWt_Univ. Qed.

Lemma SemWt_SemEq Γ (a b A : PTm) : Γ ⊨ a ∈ A Γ ⊨ b ∈ A (DJoin.R a b) Γ ⊨ a ≡ b ∈ A.
Proof.
  move ha hb heq. split //= ρ hρ.
  have {}/ha := hρ.
  have {}/hb := hρ.
  move [k][PA][hPA]hpb.
  move [][][]hpa.
  have : PA ≐ by eauto using LRFacts.functional.
  firstorder.
Qed.

Lemma SemWt_SemLEq Γ (A B : PTm) i j :
  Γ ⊨ A ∈ PUniv i Γ ⊨ B ∈ PUniv j Sub.R A B Γ ⊨ A ≲ B.
Proof.
  move ha hb heq. split //.
  exists (Nat.max i j).
  have [? ?] : i Nat.max i j j Nat.max i j by lia.
  move ρ hρ.
  have {}/ha := hρ.
  have {}/hb := hρ.
  move [k][PA][/= /LRFacts.Univ_inv [ hPA]]hpb.
  move [][][/= /LRFacts.Univ_inv [ ]]hpa.
  setoid_rewrite in hpb {}.
  setoid_rewrite in hpa {}.
  move : hpb []hPA'.
  move : hpa []hPB'.
  exists , .
  split; apply : LRFacts.cumulative; eauto.
Qed.

Structural properties about closing substitutions and semantic typing

Lemma ρ_ok_id Γ :
  ρ_ok Γ VarPTm.
Proof.
  rewrite /ρ_ok.
  hauto q:on use:LRFacts.adequacy ctrs:SNe.
Qed.

Lemma ρ_ok_cons i Γ ρ a PA A :
  ⟦ subst_PTm ρ A ⟧ i ↘ PA PA a
  ρ_ok Γ ρ
  ρ_ok (cons A Γ) (scons a ρ).
Proof.
  move .
  rewrite /ρ_ok.
  case [|j]; cycle 1.
  - move m . asimpl ?.
    inversion 1; subst; asimpl.
    hauto lq:on unfold:ρ_ok.
  - move m .
    inversion 1; subst. asimpl h.
    have ? : ≐ PA by eauto using LRFacts.functional.
    firstorder.
Qed.

Lemma ρ_ok_cons' i Γ ρ a PA A Δ :
  Δ = (cons A Γ)
  ⟦ subst_PTm ρ A ⟧ i ↘ PA PA a
  ρ_ok Γ ρ
  ρ_ok Δ (scons a ρ).
Proof. move . apply ρ_ok_cons. Qed.

Lemma ρ_ok_renaming (Γ : list PTm) ρ :
   (Δ : list PTm) ξ,
    renaming_ok Γ Δ ξ
    ρ_ok Γ ρ
    ρ_ok Δ (funcomp ρ ξ).
Proof.
  move Δ ξ hξ hρ.
  rewrite /ρ_ok i m' A PA.
  rewrite /renaming_ok in hξ.
  rewrite /ρ_ok in hρ.
  move h.
  rewrite /funcomp.
  eapply hρ with (k := m'); eauto.
  move : h. by asimpl.
Qed.

Lemma renaming_SemWt Γ a A :
  Γ ⊨ a ∈ A
   Δ (ξ : ),
    renaming_ok Δ Γ ξ
    Δ ⊨ ren_PTm ξ a ∈ ren_PTm ξ A.
Proof.
  rewrite /SemWt h Δ ξ hξ ρ hρ.
  have /h hρ' : (ρ_ok Γ (funcomp ρ ξ)) by eauto using ρ_ok_renaming.
  hauto q:on solve+:(by asimpl).
Qed.

Definition smorphing_ok Δ Γ ρ :=
   ξ, ρ_ok Δ ξ ρ_ok Γ (funcomp (subst_PTm ξ) ρ).

Lemma smorphing_ok_refl Δ : smorphing_ok Δ Δ VarPTm.
  rewrite /smorphing_ok ξ. apply.
Qed.

Lemma ρ_ok_ext ρ0 ρ1 Γ :
  ( x, ρ0 x = ρ1 x)
  ρ_ok Γ ρ0 ρ_ok Γ ρ1.
Proof.
  rewrite /ρ_ok ?.
  have : A, subst_PTm ρ0 A = subst_PTm ρ1 A by eauto using ext_PTm.
  hauto l:on.
Qed.

Lemma smorphing_ren Ξ Δ Γ
  (ρ : PTm) (ξ : ) :
  renaming_ok Ξ Δ ξ smorphing_ok Δ Γ ρ
  smorphing_ok Ξ Γ (funcomp (ren_PTm ξ) ρ).
Proof.
  move hξ hρ τ.
  move /ρ_ok_renaming : hξ /[apply].
  move h.
  rewrite /smorphing_ok in hρ.
  asimpl.
  set u := funcomp _ _.
  have : x, u x = funcomp (subst_PTm (funcomp τ ξ)) ρ x.
  subst u. by asimpl.
  hauto lq:on use:ρ_ok_ext.
Qed.

Lemma smorphing_ext Δ Γ (ρ : PTm) (a : PTm) (A : PTm) :
  smorphing_ok Δ Γ ρ
  Δ ⊨ a ∈ subst_PTm ρ A
  smorphing_ok
    Δ (cons A Γ) (scons a ρ).
Proof.
  move h ha τ. move /[dup] hτ.
  move : ha /[apply].
  move [k][PA][].
  apply h in hτ.
  case [|i]; cycle 1.
  - move . asimpl. rewrite {2}/funcomp.
    asimpl. elim /lookup_inv //= _.
    move Γ0 B + [?][? ?]?. subst.
    asimpl.
    move : hτ; by repeat move/[apply].
  - move . asimpl. rewrite {2}/funcomp. asimpl.
    elim /lookup_inv //=_ Γ0 _ [? ?] ?. subst. asimpl.
    move . suff : ≐ PA by firstorder.
    move : . asimpl.
    eauto using LRFacts.functional.
Qed.

Lemma morphing_SemWt : Γ (a A : PTm ),
    Γ ⊨ a ∈ A Δ (ρ : PTm ),
      smorphing_ok Δ Γ ρ Δ ⊨ subst_PTm ρ a ∈ subst_PTm ρ A.
Proof.
  move Γ a A ha Δ ρ hρ τ hτ.
  have {}/hρ {}/ha := hτ.
  asimpl. eauto.
Qed.

Lemma morphing_SemWt_Univ : Γ (a : PTm) i,
    Γ ⊨ a ∈ PUniv i Δ (ρ : PTm),
      smorphing_ok Δ Γ ρ Δ ⊨ subst_PTm ρ a ∈ PUniv i.
Proof.
  move Γ a i ha Δ ρ.
  have : PUniv i = subst_PTm ρ (PUniv i) by reflexivity.
  by apply morphing_SemWt.
Qed.

Lemma weakening_Sem Γ (a : PTm) A B i
  (h0 : Γ ⊨ B ∈ PUniv i)
  (h1 : Γ ⊨ a ∈ A) :
   (cons B Γ) ⊨ ren_PTm shift a ∈ ren_PTm shift A.
Proof.
  apply : renaming_SemWt; eauto.
  hauto lq:on ctrs:lookup unfold:renaming_ok.
Qed.

Lemma weakening_Sem_Univ Γ (a : PTm) B i j
  (h0 : Γ ⊨ B ∈ PUniv i)
  (h1 : Γ ⊨ a ∈ PUniv j) :
   (cons B Γ) ⊨ ren_PTm shift a ∈ PUniv j.
Proof.
  move : weakening_Sem ; repeat move/[apply]. done.
Qed.

Reserved Notation "⊨ Γ" (at level 70).

Inductive SemWff : list PTm Prop :=
| SemWff_nil :
  ⊨ nil
| SemWff_cons Γ A i :
  ⊨ Γ
  Γ ⊨ A ∈ PUniv i
  (* -------------- *)
  ⊨ (cons A Γ)
where "⊨ Γ" := (SemWff Γ).

(* Semantic context wellformedness *)
Lemma SemWff_lookup Γ :
  ⊨ Γ
   (i : ) A, lookup i Γ A j, Γ ⊨ A ∈ PUniv j.
Proof.
  move h. elim : Γ / h.
  - by inversion 1.
  - move Γ A i hΓ ihΓ hA j B.
    elim /lookup_inv //=_.
    + move ? ? ? [*]. subst.
      eauto using weakening_Sem_Univ.
    + move Γ0 hl ? [*]. subst.
      move : ihΓ hl /[apply]. move [j ].
      eauto using weakening_Sem_Univ.
Qed.

Lemma SemWt_SN Γ (a : PTm) A :
  Γ ⊨ a ∈ A
  SN a SN A.
Proof.
  move h.
  have {}/h := ρ_ok_id Γ h.
  have : SN (subst_PTm VarPTm A) by hauto l:on use:LRFacts.adequacy.
  have : SN (subst_PTm VarPTm a)by hauto l:on use:LRFacts.adequacy.
  by asimpl.
Qed.

Lemma SemEq_SN_Join Γ (a b A : PTm) :
  Γ ⊨ a ≡ b ∈ A
  SN a SN b SN A DJoin.R a b.
Proof. hauto l:on use:SemEq_SemWt, SemWt_SN. Qed.

Lemma SemLEq_SN_Sub Γ (a b : PTm) :
  Γ ⊨ a ≲ b
  SN a SN b Sub.R a b.
Proof. hauto l:on use:SemLEq_SemWt, SemWt_SN. Qed.

Semantic typing rules

Each rule corresponds to one case of the fundamental theorem
Lemma ST_Var' Γ (i : ) A j :
  lookup i Γ A
  Γ ⊨ A ∈ PUniv j
  Γ ⊨ VarPTm i ∈ A.
Proof.
  move hl /SemWt_Univ h.
  rewrite /SemWt ρ /[dup] hρ {}/h [S hS].
  exists j,S.
  asimpl. hauto q:on unfold:ρ_ok.
Qed.

Lemma ST_Var Γ (i : ) A :
  ⊨ Γ
  lookup i Γ A
  Γ ⊨ VarPTm i ∈ A.
Proof. hauto l:on use:ST_Var', SemWff_lookup. Qed.

Lemma ST_Bind' Γ i j p (A : PTm) (B : PTm) :
  Γ ⊨ A ∈ PUniv i
  (cons A Γ) ⊨ B ∈ PUniv j
  Γ ⊨ PBind p A B ∈ PUniv (max i j).
Proof.
  move /SemWt_Univ /SemWt_Univ .
  apply SemWt_Univ ρ hρ.
  move / : (hρ){} [S hS].
  eexists /=.
  have ? : i Nat.max i j by lia.
  apply LRFacts.Bind_nopf; eauto.
  - eauto using LRFacts.cumulative.
  - move *. asimpl. hauto l:on use:LRFacts.cumulative, ρ_ok_cons.
Qed.

Lemma ST_Bind Γ i p (A : PTm) (B : PTm) :
  Γ ⊨ A ∈ PUniv i
  cons A Γ ⊨ B ∈ PUniv i
  Γ ⊨ PBind p A B ∈ PUniv i.
Proof.
  move .
  replace i with (max i i) by lia.
  move : .
  apply ST_Bind'.
Qed.

Lemma ST_Abs Γ (a : PTm) A B i :
  Γ ⊨ PBind PPi A B ∈ (PUniv i)
  (cons A Γ) ⊨ a ∈ B
  Γ ⊨ PAbs a ∈ PBind PPi A B.
Proof.
  rename a into b.
  move /SemWt_Univ + hb ρ hρ.
  move /(_ _ hρ) [PPi hPPi].
  exists i, PPi. split //.
  simpl in hPPi.
  move /LRFacts.Bind_inv_nopf : hPPi.
  move [PA [hPA [hTot h]]]. rewrite h {PPi h}. simpl.
  move a PB ha. asimpl hPB.
  move : ρ_ok_cons (hPA) (hρ) (ha). repeat move/[apply].
  move /hb.
  intros (m & & & ).
  have h : ≐ PB by eauto using LRFacts.functional.
  rewrite h in .
  apply : LRFacts.back_clos; eauto.
  apply N_β'. by asimpl.
  move : ha hPA. clear. hauto q:on use:LRFacts.adequacy.
Qed.

Lemma ST_App Γ (b a : PTm) A B :
  Γ ⊨ b ∈ PBind PPi A B
  Γ ⊨ a ∈ A
  Γ ⊨ PApp b a ∈ subst_PTm (scons a VarPTm) B.
Proof.
  move hf hb ρ hρ.
  move /(_ ρ hρ) : hf; intros (i & PPi & hPi & hf).
  move /(_ ρ hρ) : hb; intros (j & PA & hPA & hb).
  simpl in hPi.
  move /LRFacts.Bind_inv_nopf : hPi. intros ( & & hTot & ).
  rewrite in hf {PPi }.
  have h : ≐ PA by eauto using LRFacts.functional.
  simpl in hf. rewrite /ProdSpace in hf.
  setoid_rewrite h in hf.
  setoid_rewrite h in hTot.
  move : hf (hb) /[apply].
  move : hTot hb /[apply].
  asimpl. hauto lq:on.
Qed.

Lemma ST_App' Γ (b a : PTm) A B U :
  U = subst_PTm (scons a VarPTm) B
  Γ ⊨ b ∈ PBind PPi A B
  Γ ⊨ a ∈ A
  Γ ⊨ PApp b a ∈ U.
Proof. move . apply ST_App. Qed.

Lemma ST_Pair Γ (a b : PTm) A B i :
  Γ ⊨ PBind PSig A B ∈ (PUniv i)
  Γ ⊨ a ∈ A
  Γ ⊨ b ∈ subst_PTm (scons a VarPTm) B
  Γ ⊨ PPair a b ∈ PBind PSig A B.
Proof.
  move /SemWt_Univ + ha hb ρ hρ.
  move /(_ _ hρ) [PPi hPPi].
  exists i, PPi. split //.
  simpl in hPPi.
  move /LRFacts.Bind_inv_nopf : hPPi.
  move [PA [hPA [hTot h]]]. setoid_rewrite h {PPi h} /=.
  rewrite /SumSpace. right.
  exists (subst_PTm ρ a), (subst_PTm ρ b).
  split.
  - apply rtc_refl.
  - move /ha : (hρ){ha}.
    move [m][][].
    move /hb : (hρ){hb}.
    move [k][PB][].
    have h : ≐ PA by eauto using LRFacts.functional.
    setoid_rewrite h.
    split // .
    move : . asimpl *.
    have ? : ≐ PB by eauto using LRFacts.functional.
    firstorder.
Qed.

Lemma N_Projs p (a b : PTm) :
  rtc TRedSN a b
  rtc TRedSN (PProj p a) (PProj p b).
Proof. induction 1; hauto lq:on ctrs:rtc, TRedSN. Qed.

Lemma ST_Proj1 Γ (a : PTm) A B :
  Γ ⊨ a ∈ PBind PSig A B
  Γ ⊨ PProj PL a ∈ A.
Proof.
  move h ρ /[dup]hρ {}/h [m][PA][/= /LRFacts.Bind_inv_nopf ].
  move : [S][][]h. setoid_rewrite h in {PA h}.
  move : /=.
  rewrite /SumSpace.
  case.
  - move [v [ ]].
    have {} : rtc TRedSN (PProj PL (subst_PTm ρ a)) (PProj PL v) by hauto lq:on use:N_Projs.
    have {} : SNe (PProj PL v) by hauto lq:on ctrs:SNe.
    hauto q:on use:LRFacts.back_closs,LRFacts.adequacy.
  - move [ [ [ [ ]]]].
    exists m, S. split //=.
    have {} : rtc TRedSN (PProj PL (subst_PTm ρ a)) (PProj PL (PPair )) by eauto using N_Projs.
    have ? : rtc TRedSN (PProj PL (PPair )) by hauto q:on ctrs:rtc, TRedSN use:LRFacts.adequacy.
    have : rtc TRedSN (PProj PL (subst_PTm ρ a)) by hauto q:on ctrs:rtc use:@relations.rtc_r.
    move h.
    apply : LRFacts.back_closs; eauto.
Qed.

Lemma ST_Proj2 Γ (a : PTm) A B :
  Γ ⊨ a ∈ PBind PSig A B
  Γ ⊨ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B.
Proof.
  move h ρ hρ.
  move : (hρ) {}/h [m][PA][/= /LRFacts.Bind_inv_nopf ].
  move : [S][][]h. setoid_rewrite h in {PA h}.
  move : /=.
  rewrite /SumSpace.
  case.
  - move h.
    move : h [v [ ]].
    have hp : p, SNe (PProj p v) by hauto lq:on ctrs:SNe.
    have hp' : p, rtc TRedSN (PProj p(subst_PTm ρ a)) (PProj p v) by eauto using N_Projs.
    have := hp PL. have := hp PR {hp}.
    have := hp' PL. have := hp' PR {hp'}.
    have : S (PProj PL (subst_PTm ρ a)). apply : LRFacts.back_closs; eauto. hauto q:on use:LRFacts.adequacy.
    move / [PB]. asimpl hPB.
    do 2 eexists. split; eauto.
    apply : LRFacts.back_closs; eauto. hauto q:on use:LRFacts.adequacy.
  - move [ [ [ [ ]]]].
    have h3_dup := .
    specialize with (1 := ).
    move : [PB hPB].
    have hr : p, rtc TRedSN (PProj p (subst_PTm ρ a)) (PProj p (PPair )) by hauto l:on use: N_Projs.
    have hSN : SN by move : ; clear; hauto q:on use:LRFacts.adequacy.
    have hSN' : SN by hauto q:on use:LRFacts.adequacy.
    have hrl : TRedSN (PProj PL (PPair )) by hauto lq:on ctrs:TRedSN.
    have hrr : TRedSN (PProj PR (PPair )) by hauto lq:on ctrs:TRedSN.
    exists m, PB.
    asimpl. split.
    + have hr' : rtc TRedSN (PProj PL (subst_PTm ρ a)) by hauto l:on use:@relations.rtc_r.
      have : S (PProj PL (subst_PTm ρ a)) by hauto lq:on use:LRFacts.back_closs.
      move {}/h3_dup.
      move []. asimpl .
      suff h : PB ≐ by hauto l:on db:InterpUniv.
      move : hPB. asimpl hPB.
      suff : DJoin.R (subst_PTm (scons (PProj PL (subst_PTm ρ a)) ρ) B) (subst_PTm (scons ρ) B).
      hauto lq:on use:LRFacts.join.
      apply DJoin.cong.
      apply DJoin.FromRedSNs.
      hauto lq:on ctrs:rtc.
    + hauto lq:on use:@relations.rtc_r, LRFacts.back_closs.
Qed.

Lemma ST_Conv' Γ (a : PTm) A B i :
  Γ ⊨ a ∈ A
  Γ ⊨ B ∈ PUniv i
  Sub.R A B
  Γ ⊨ a ∈ B.
Proof.
  move ha /SemWt_Univ h .
  move ρ hρ.
  have {} : Sub.R (subst_PTm ρ A) (subst_PTm ρ B) by
    eauto using Sub.substing.
  move /ha : (hρ){ha} [m [PA [ ]]].
  move /h : (hρ){h} [S hS].
  have : x, PA x S x.
  move : LRFacts.sub hS; by repeat move/[apply].
  hauto lq:on.
Qed.

Lemma ST_Conv_E Γ (a : PTm) A B i :
  Γ ⊨ a ∈ A
  Γ ⊨ B ∈ PUniv i
  DJoin.R A B
  Γ ⊨ a ∈ B.
Proof.
  hauto l:on use:ST_Conv', Sub.FromJoin.
Qed.

Lemma ST_Conv Γ (a : PTm) A B :
  Γ ⊨ a ∈ A
  Γ ⊨ A ≲ B
  Γ ⊨ a ∈ B.
Proof. hauto l:on use:ST_Conv', SemLEq_SemWt. Qed.

Lemma SE_Refl Γ (a : PTm) A :
  Γ ⊨ a ∈ A
  Γ ⊨ a ≡ a ∈ A.
Proof. hauto lq:on unfold:SemWt,SemEq use:DJoin.refl. Qed.

Lemma SE_Symmetric Γ (a b : PTm) A :
  Γ ⊨ a ≡ b ∈ A
  Γ ⊨ b ≡ a ∈ A.
Proof. hauto q:on unfold:SemEq. Qed.

Lemma SE_Transitive Γ (a b c : PTm) A :
  Γ ⊨ a ≡ b ∈ A
  Γ ⊨ b ≡ c ∈ A
  Γ ⊨ a ≡ c ∈ A.
Proof.
  move ha hb.
  apply SemEq_SemWt in ha, hb.
  have ? : SN b by hauto l:on use:SemWt_SN.
  apply SemWt_SemEq; try tauto.
  hauto l:on use:DJoin.transitive.
Qed.

Definition Γ_sub' Γ Δ := ρ, ρ_ok Δ ρ ρ_ok Γ ρ.

Definition Γ_eq' Γ Δ := ρ, ρ_ok Δ ρ ρ_ok Γ ρ.

Lemma Γ_sub'_refl Γ : Γ_sub' Γ Γ.
  rewrite /Γ_sub'. sfirstorder b:on. Qed.

Lemma Γ_sub'_cons Γ Δ A B i j :
  Sub.R B A
  Γ_sub' Γ Δ
  Γ ⊨ A ∈ PUniv i
  Δ ⊨ B ∈ PUniv j
  Γ_sub' (cons A Γ) (cons B Δ).
Proof.
  move hsub hsub' hA hB ρ hρ.
  move k k' PA.
  have hρ_inv : ρ_ok Δ (funcomp ρ shift).
  move : hρ. clear.
  move hρ i.
  (* specialize (hρ (shift i)). *)
  move k A PA.
  move /there. move /(_ B).
  rewrite /ρ_ok in hρ.
  move /hρ. asimpl. by apply.
  elim /lookup_inv //=hl.
  move Γ0 ? [? ?] ?. subst.
  - asimpl.
    move h.
    have {}/hsub' hρ' := hρ_inv.
    move /SemWt_Univ : (hA) (hρ') /[apply].
    move [S]hS.
    move /SemWt_Univ : (hB) (hρ_inv)/[apply].
    move [].
    move /(_ var_zero j (ren_PTm shift B) ) : hρ (). asimpl.
    move /[apply].
    move /(_ ltac:(apply here)).
    move *.
    suff : x, x PA x by firstorder.
    apply : LRFacts.sub; eauto.
    by apply Sub.substing.
  - rewrite /Γ_sub' in hsub'.
    asimpl.
    move Γ0 ? [? ?]?. subst.
    move /(_ (funcomp ρ shift) hρ_inv) in hsub'.
    move : hsub' /[apply]. move /[apply]. by asimpl.
Qed.

Lemma Γ_sub'_SemWt Γ Δ a A :
  Γ_sub' Γ Δ
  Γ ⊨ a ∈ A
  Δ ⊨ a ∈ A.
Proof.
  move hs ha ρ hρ.
  have {}/hs hρ' := hρ.
  hauto l:on.
Qed.

Lemma Γ_eq_sub Γ Δ : Γ_eq' Γ Δ Γ_sub' Γ Δ Γ_sub' Δ Γ.
Proof. rewrite /Γ_eq' /Γ_sub'. hauto l:on. Qed.

Lemma Γ_eq'_cons Γ Δ A B i j :
  DJoin.R B A
  Γ_eq' Γ Δ
  Γ ⊨ A ∈ PUniv i
  Δ ⊨ B ∈ PUniv j
  Γ_eq' (cons A Γ) (cons B Δ).
Proof.
  move h.
  have {h} [ ] : Sub.R A B Sub.R B A by hauto lq:on use:Sub.FromJoin, DJoin.symmetric.
  repeat rewrite Γ_eq_sub.
  hauto l:on use:Γ_sub'_cons.
Qed.

Lemma Γ_eq'_refl Γ : Γ_eq' Γ Γ.
Proof. rewrite /Γ_eq'. firstorder. Qed.

Lemma SE_Bind' Γ i j p (A0 A1 : PTm) B0 B1 :
  Γ ⊨ ≡ ∈ PUniv i
  cons Γ ⊨ ≡ ∈ PUniv j
  Γ ⊨ PBind p ≡ PBind p ∈ PUniv (max i j).
Proof.
  move hA hB.
  apply SemEq_SemWt in hA, hB.
  apply SemWt_SemEq; last by hauto l:on use:DJoin.BindCong.
  hauto l:on use:ST_Bind'.
  apply ST_Bind'; first by tauto.
  move ρ hρ.
  suff : ρ_ok (cons Γ) ρ by hauto l:on.
  move : hρ.
  suff : Γ_sub' ( :: Γ) ( :: Γ) by hauto l:on unfold:Γ_sub'.
  apply : Γ_sub'_cons.
  apply /Sub.FromJoin /DJoin.symmetric. tauto.
  apply Γ_sub'_refl. hauto lq:on.
  hauto lq:on.
Qed.

Lemma SE_Bind Γ i p (A0 A1 : PTm) B0 B1 :
  Γ ⊨ ≡ ∈ PUniv i
  cons Γ ⊨ ≡ ∈ PUniv i
  Γ ⊨ PBind p ≡ PBind p ∈ PUniv i.
Proof.
  move *. replace i with (max i i) by lia. auto using SE_Bind'.
Qed.

Lemma SE_Abs Γ (a b : PTm) A B i :
  Γ ⊨ PBind PPi A B ∈ (PUniv i)
  cons A Γ ⊨ a ≡ b ∈ B
  Γ ⊨ PAbs a ≡ PAbs b ∈ PBind PPi A B.
Proof.
  move hPi /SemEq_SemWt [ha][hb]he.
  apply SemWt_SemEq; eauto using DJoin.AbsCong, ST_Abs.
Qed.

Lemma SBind_inv1 Γ i p (A : PTm) B :
  Γ ⊨ PBind p A B ∈ PUniv i
  Γ ⊨ A ∈ PUniv i.
  move /SemWt_Univ h. apply SemWt_Univ.
  hauto lq:on rew:off use:LRFacts.Bind_inv.
Qed.

Lemma SE_AppEta Γ (b : PTm) A B i :
  Γ ⊨ PBind PPi A B ∈ (PUniv i)
  Γ ⊨ b ∈ PBind PPi A B
  Γ ⊨ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B.
Proof.
  move . apply SemWt_SemEq; eauto.
  apply : ST_Abs; eauto.
  have hA : Γ ⊨ A ∈ PUniv i by eauto using SBind_inv1.
  eapply ST_App' with (A := ren_PTm shift A)(B:= ren_PTm (upRen_PTm_PTm shift) B). asimpl. by rewrite subst_scons_id.
  2 : {
    apply : ST_Var'.
    apply here.
    apply : weakening_Sem_Univ; eauto.
  }
  change (PBind PPi (ren_PTm shift A) (ren_PTm (upRen_PTm_PTm shift) B)) with
    (ren_PTm shift (PBind PPi A B)).
  apply : weakening_Sem; eauto.
  hauto q:on ctrs:rtc,RERed.R.
Qed.

Lemma SE_AppAbs Γ (a : PTm) b A B i:
  Γ ⊨ PBind PPi A B ∈ PUniv i
  Γ ⊨ b ∈ A
  (cons A Γ) ⊨ a ∈ B
  Γ ⊨ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B.
Proof.
  move h . apply SemWt_SemEq; eauto using ST_App, ST_Abs.
  move ρ hρ.
  have {}/ := hρ.
  move [k][PA][hPA]hb.
  move : ρ_ok_cons hPA hb (hρ); repeat move/[apply].
  move {}/.
  by asimpl.
  apply DJoin.FromRRed0.
  apply RRed.AppAbs.
Qed.

Lemma SE_Conv' Γ (a b : PTm) A B i :
  Γ ⊨ a ≡ b ∈ A
  Γ ⊨ B ∈ PUniv i
  Sub.R A B
  Γ ⊨ a ≡ b ∈ B.
Proof.
  move /SemEq_SemWt [ha][hb]he hB hAB.
  apply SemWt_SemEq; eauto using ST_Conv'.
Qed.

Lemma SE_Conv Γ (a b : PTm) A B :
  Γ ⊨ a ≡ b ∈ A
  Γ ⊨ A ≲ B
  Γ ⊨ a ≡ b ∈ B.
Proof.
  move h /SemLEq_SemWt [][][ha]hb.
  eauto using SE_Conv'.
Qed.

Lemma SBind_inst Γ p i (A : PTm) B (a : PTm) :
  Γ ⊨ a ∈ A
  Γ ⊨ PBind p A B ∈ PUniv i
  Γ ⊨ subst_PTm (scons a VarPTm) B ∈ PUniv i.
Proof.
  move ha /SemWt_Univ hb.
  apply SemWt_Univ.
  move ρ hρ.
  have {}/hb := hρ.
  asimpl. move /= [S hS].
  move /LRFacts.Bind_inv_nopf : hS.
  move [PA][hPA][hPF]?. subst.
  have {}/ha := hρ.
  move [k][][]ha.
  have h : ≐ PA by eauto using LRFacts.functional. setoid_rewrite h in ha.
  have {}/hPF := ha.
  move [PB]. asimpl.
  hauto lq:on.
Qed.

Lemma SE_Pair Γ (a0 a1 b0 b1 : PTm) A B i :
  Γ ⊨ PBind PSig A B ∈ (PUniv i)
  Γ ⊨ ≡ ∈ A
  Γ ⊨ ≡ ∈ subst_PTm (scons VarPTm) B
  Γ ⊨ PPair ≡ PPair ∈ PBind PSig A B.
Proof.
  move h /SemEq_SemWt [][]hae /SemEq_SemWt [][]hbe.
  apply SemWt_SemEq; eauto using ST_Pair, DJoin.PairCong, SBind_inst, DJoin.cong, ST_Conv_E, ST_Pair.
Qed.

Lemma SE_Proj1 Γ (a b : PTm) A B :
  Γ ⊨ a ≡ b ∈ PBind PSig A B
  Γ ⊨ PProj PL a ≡ PProj PL b ∈ A.
Proof.
  move /SemEq_SemWt [ha][hb]he.
  apply SemWt_SemEq; eauto using DJoin.ProjCong, ST_Proj1.
Qed.

Lemma SE_Proj2 Γ i (a b : PTm ) A B :
  Γ ⊨ PBind PSig A B ∈ (PUniv i)
  Γ ⊨ a ≡ b ∈ PBind PSig A B
  Γ ⊨ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B.
Proof.
  move hS.
  move /SemEq_SemWt [ha][hb]he.
  apply SemWt_SemEq; eauto using DJoin.ProjCong, ST_Proj2.
  have h : Γ ⊨ PProj PR b ∈ subst_PTm (scons (PProj PL b) VarPTm) B by eauto using ST_Proj2.
  apply : ST_Conv_E. apply h.
  apply : SBind_inst. eauto using ST_Proj1.
  eauto.
  hauto lq:on use: DJoin.cong, DJoin.ProjCong.
Qed.

Lemma ST_Nat Γ i :
  Γ ⊨ PNat ∈ PUniv i.
Proof.
  move ?. apply SemWt_Univ. move ρ hρ.
  eexists. by apply InterpUniv_Nat.
Qed.

Lemma ST_Zero Γ :
  Γ ⊨ PZero ∈ PNat.
Proof.
  move ρ hρ. exists 0, SNat. simpl. split.
  apply InterpUniv_Nat.
  apply S_Zero.
Qed.

Lemma ST_Suc Γ (a : PTm) :
  Γ ⊨ a ∈ PNat
  Γ ⊨ PSuc a ∈ PNat.
Proof.
  move ha ρ.
  move : ha /[apply] /=.
  move [k][PA][ ].
  have h : PA ≐ SNat by eauto using LRFacts.Nat_inv.
  setoid_rewrite h in .
  exists 0, SNat. split. apply InterpUniv_Nat.
  eauto using S_Suc.
Qed.

Lemma sn_unmorphing' : ( (a : PTm) (s : SN a), (ρ : PTm) b, a = subst_PTm ρ b SN b).
Proof. hauto l:on use:sn_unmorphing. Qed.

Lemma sn_bot_up (a : PTm) i (ρ : PTm) :
  SN (subst_PTm (scons (VarPTm i) ρ) a) SN (subst_PTm (up_PTm_PTm ρ) a).
  rewrite /up_PTm_PTm.
  move h. eapply sn_unmorphing' with (ρ := (scons (VarPTm i) VarPTm)); eauto.
  by asimpl.
Qed.

Lemma sn_bot_up2 (a : PTm) j i (ρ : PTm) :
  SN ((subst_PTm (scons (VarPTm j) (scons (VarPTm i) ρ)) a)) SN (subst_PTm (up_PTm_PTm (up_PTm_PTm ρ)) a).
  rewrite /up_PTm_PTm.
  move h. eapply sn_unmorphing' with (ρ := (scons (VarPTm j) (scons (VarPTm i) VarPTm))); eauto.
  by asimpl.
Qed.

Lemma SNat_SN (a : PTm) : SNat a SN a.
  induction 1; hauto lq:on ctrs:SN. Qed.

Lemma ST_Ind Γ P (a : PTm) b c i :
  (cons PNat Γ) ⊨ P ∈ PUniv i
  Γ ⊨ a ∈ PNat
  Γ ⊨ b ∈ subst_PTm (scons PZero VarPTm) P
  (cons P (cons PNat Γ)) ⊨ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P)
  Γ ⊨ PInd P a b c ∈ subst_PTm (scons a VarPTm) P.
Proof.
  move hA hc ha hb ρ hρ.
  move /(_ ρ hρ) : ha [m][PA][].
  move /(_ ρ hρ) : hc [n][][h].
  have {}h : ≐ SNat by eauto using LRFacts.Nat_inv.
  setoid_rewrite h.
  simpl.
  (* Use localiaztion to block asimpl from simplifying pind *)
  set x := PInd _ _ _ _. asimpl. subst x. move : {a} (subst_PTm ρ a) .
  move : (subst_PTm ρ b) {}b .
  move u hu.
  have hρb : ρ_ok (cons PNat Γ) (scons (VarPTm var_zero) ρ) by apply : ρ_ok_cons; hauto lq:on ctrs:SNat, SNe use:(@InterpUniv_Nat 0).
  have hρbb : ρ_ok (cons P (cons PNat Γ)) (scons (VarPTm var_zero) (scons (VarPTm var_zero) ρ)).
  move /SemWt_Univ /(_ _ hρb) : hA [S ?].
  apply : ρ_ok_cons; eauto. sauto lq:on use:LRFacts.adequacy.

  (* have snP : SN P by hauto l:on use:SemWt_SN. *)
  have snb : SN b by hauto q:on use:LRFacts.adequacy.
  have snP : SN (subst_PTm (up_PTm_PTm ρ) P)
    by eapply sn_bot_up; move : hA hρb /[apply]; hauto lq:on use:LRFacts.adequacy.
  have snc : SN (subst_PTm (up_PTm_PTm (up_PTm_PTm ρ)) c)
    by apply: sn_bot_up2; move : hb hρbb /[apply]; hauto lq:on use:LRFacts.adequacy.

  elim : u /hu.
  + exists m, PA. split.
    * move : . by asimpl.
    * apply : LRFacts.back_clos; eauto.
      apply N_IndZero; eauto.
  + move a snea.
    have hρ' : ρ_ok (cons PNat Γ) (scons a ρ)by
      apply : ρ_ok_cons; eauto using (InterpUniv_Nat 0); hauto ctrs:SNat.
    move /SemWt_Univ : (hA) hρ' /[apply].
    move [ ].
    exists i, . split//.
    eapply LRFacts.adequacy; eauto.
    apply N_Ind; eauto.
  + move a ha [j][S][].
    have hρ' : ρ_ok (cons PNat Γ) (scons (PSuc a) ρ)by
      apply : ρ_ok_cons; eauto using (InterpUniv_Nat 0); hauto ctrs:SNat.
    move /SemWt_Univ : (hA) (hρ') /[apply].
    move [ ].
    exists i, . split //.
    apply : LRFacts.back_clos; eauto.
    apply N_IndSuc; eauto using SNat_SN.
    move : (PInd (subst_PTm (up_PTm_PTm ρ) P) a b
              (subst_PTm (up_PTm_PTm (up_PTm_PTm ρ)) c)) .
    move r hr.
    have hρ'' : ρ_ok
                   (cons P (cons PNat Γ)) (scons r (scons a ρ)) by
      eauto using ρ_ok_cons, (InterpUniv_Nat 0).
    move : hb hρ'' /[apply].
    move [k][][].
    move : . asimpl ?.
    have ? : ≐ by eauto using LRFacts.functional.
    firstorder.
  + move a a' hr ha' [k][][].
    have : ρ_ok (cons PNat Γ) (scons a ρ)
      by apply : ρ_ok_cons; hauto l:on use:S_Red,(InterpUniv_Nat 0).
    move /SemWt_Univ : hA /[apply]. move [].
    exists i, . split //.
    apply : LRFacts.back_clos; eauto.
    apply N_IndCong; eauto.
    suff : ≐ by firstorder.
    suff : DJoin.R (subst_PTm (scons a' ρ) P) (subst_PTm (scons a ρ) P ) by eauto using LRFacts.join.
    apply DJoin.FromRReds.
    apply RReds.FromRPar.
    apply RPar.morphing; last by apply RPar.refl.
    eapply LoReds.FromSN_mutual in hr.
    move /LoRed.ToRRed /RPar.FromRRed in hr.
    hauto lq:on inv: use:RPar.refl.
Qed.

Lemma SE_SucCong Γ (a b : PTm) :
  Γ ⊨ a ≡ b ∈ PNat
  Γ ⊨ PSuc a ≡ PSuc b ∈ PNat.
Proof.
  move /SemEq_SemWt [ha][hb]he.
  apply SemWt_SemEq; eauto using ST_Suc.
  hauto q:on use:REReds.suc_inv, REReds.SucCong.
Qed.

Lemma SE_IndCong Γ P0 P1 (a0 a1 : PTm ) b0 b1 c0 c1 i :
  cons PNat Γ ⊨ ≡ ∈ PUniv i
  Γ ⊨ ≡ ∈ PNat
  Γ ⊨ ≡ ∈ subst_PTm (scons PZero VarPTm)
  cons (cons PNat Γ) ⊨ ≡ ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) )
  Γ ⊨ PInd ≡ PInd ∈ subst_PTm (scons VarPTm) .
Proof.
  move /SemEq_SemWt[][]hPe.
  move /SemEq_SemWt[][]hae.
  move /SemEq_SemWt[][]hbe.
  move /SemEq_SemWt[][]hce.
  apply SemWt_SemEq; eauto using ST_Ind, DJoin.IndCong.
  apply ST_Conv_E with (A := subst_PTm (scons VarPTm) ) (i := i);
    last by eauto using DJoin.cong', DJoin.symmetric.
  apply : ST_Ind; eauto. eapply ST_Conv_E with (i := i); eauto.
  apply : morphing_SemWt_Univ; eauto.
  apply smorphing_ext. rewrite /smorphing_ok.
  move ξ. rewrite /funcomp. by asimpl.
  by apply ST_Zero.
  by apply DJoin.substing.
  eapply ST_Conv_E with (i := i); eauto.
  apply : Γ_sub'_SemWt; eauto.
  apply : Γ_sub'_cons; eauto using DJoin.symmetric, Sub.FromJoin.
  apply : Γ_sub'_cons; eauto using Sub.refl, Γ_sub'_refl, (@ST_Nat _ 0).
  apply : weakening_Sem_Univ; eauto. move : .
  move /morphing_SemWt. apply. apply smorphing_ext.
  have : (funcomp VarPTm shift) = funcomp (ren_PTm shift) (VarPTm) by asimpl.
  apply : smorphing_ren; eauto using smorphing_ok_refl. hauto l:on inv:option.
  apply ST_Suc. apply ST_Var' with (j := 0). apply here.
  apply ST_Nat.
  apply DJoin.renaming. by apply DJoin.substing.
  apply : morphing_SemWt_Univ; eauto.
  apply smorphing_ext; eauto using smorphing_ok_refl.
Qed.

Lemma SE_IndZero Γ P i (b : PTm) c :
  (cons PNat Γ) ⊨ P ∈ PUniv i
  Γ ⊨ b ∈ subst_PTm (scons PZero VarPTm) P
  (cons P (cons PNat Γ)) ⊨ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P)
  Γ ⊨ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P.
Proof.
  move hP hb hc.
  apply SemWt_SemEq; eauto using ST_Zero, ST_Ind.
  apply DJoin.FromRRed0. apply RRed.IndZero.
Qed.

Lemma SE_IndSuc Γ P (a : PTm) b c i :
  (cons PNat Γ) ⊨ P ∈ PUniv i
  Γ ⊨ a ∈ PNat
  Γ ⊨ b ∈ subst_PTm (scons PZero VarPTm) P
  (cons P (cons PNat Γ)) ⊨ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P)
  Γ ⊨ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P.
Proof.
  move hP ha hb hc.
  apply SemWt_SemEq; eauto using ST_Suc, ST_Ind.
  set Δ := (X in X ⊨ _ ∈ _) in hc.
  have : smorphing_ok Γ Δ (scons (PInd P a b c) (scons a VarPTm)).
  apply smorphing_ext. apply smorphing_ext. apply smorphing_ok_refl.
  done. eauto using ST_Ind.
  move : morphing_SemWt hc; repeat move/[apply].
  by asimpl.
  apply DJoin.FromRRed0.
  apply RRed.IndSuc.
Qed.

Lemma SE_ProjPair1 Γ (a b : PTm) A B i :
  Γ ⊨ PBind PSig A B ∈ (PUniv i)
  Γ ⊨ a ∈ A
  Γ ⊨ b ∈ subst_PTm (scons a VarPTm) B
  Γ ⊨ PProj PL (PPair a b) ≡ a ∈ A.
Proof.
  move .
  apply SemWt_SemEq; eauto using ST_Proj1, ST_Pair.
  apply DJoin.FromRRed0. apply RRed.ProjPair.
Qed.

Lemma SE_ProjPair2 Γ (a b : PTm) A B i :
  Γ ⊨ PBind PSig A B ∈ (PUniv i)
  Γ ⊨ a ∈ A
  Γ ⊨ b ∈ subst_PTm (scons a VarPTm) B
  Γ ⊨ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B.
Proof.
  move .
  apply SemWt_SemEq; eauto using ST_Proj2, ST_Pair.
  apply : ST_Conv_E. apply : ST_Proj2; eauto. apply : ST_Pair; eauto.
  hauto l:on use:SBind_inst.
  apply DJoin.cong. apply DJoin.FromRRed0. apply RRed.ProjPair.
  apply DJoin.FromRRed0. apply RRed.ProjPair.
Qed.

Lemma SE_PairEta Γ (a : PTm) A B i :
  Γ ⊨ PBind PSig A B ∈ (PUniv i)
  Γ ⊨ a ∈ PBind PSig A B
  Γ ⊨ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B.
Proof.
  move h. apply SemWt_SemEq; eauto.
  apply : ST_Pair; eauto using ST_Proj1, ST_Proj2.
  rewrite /DJoin.R. hauto lq:on ctrs:rtc,RERed.R.
Qed.

Lemma SE_PairExt Γ (a b : PTm) A B i :
  Γ ⊨ PBind PSig A B ∈ PUniv i
  Γ ⊨ a ∈ PBind PSig A B
  Γ ⊨ b ∈ PBind PSig A B
  Γ ⊨ PProj PL a ≡ PProj PL b ∈ A
  Γ ⊨ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B
  Γ ⊨ a ≡ b ∈ PBind PSig A B.
Proof.
  move ha hb .
  suff h : Γ ⊨ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B
           Γ ⊨ PPair (PProj PL b) (PProj PR b) ≡ b ∈ PBind PSig A B
           Γ ⊨ PPair (PProj PL a) (PProj PR a) ≡ PPair (PProj PL b) (PProj PR b) ∈ PBind PSig A B
    by decompose [and] h; eauto using SE_Transitive, SE_Symmetric.
  eauto 20 using SE_PairEta, SE_Symmetric, SE_Pair.
Qed.

Lemma SE_FunExt Γ (a b : PTm) A B i :
  Γ ⊨ PBind PPi A B ∈ PUniv i
  Γ ⊨ a ∈ PBind PPi A B
  Γ ⊨ b ∈ PBind PPi A B
  A :: Γ ⊨ PApp (ren_PTm shift a) (VarPTm var_zero) ≡ PApp (ren_PTm shift b) (VarPTm var_zero) ∈ B
  Γ ⊨ a ≡ b ∈ PBind PPi A B.
Proof.
  move hpi ha hb he.
  move : SE_Abs (hpi) he. repeat move/[apply]. move he.
  have /SE_Symmetric : Γ ⊨ PAbs (PApp (ren_PTm shift a) (VarPTm var_zero)) ≡ a ∈ PBind PPi A B by eauto using SE_AppEta.
  have : Γ ⊨ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B by eauto using SE_AppEta.
  eauto using SE_Transitive.
Qed.

Lemma SE_Nat Γ (a b : PTm) :
  Γ ⊨ a ≡ b ∈ PNat
  Γ ⊨ PSuc a ≡ PSuc b ∈ PNat.
Proof.
  move /SemEq_SemWt [ha][hb]hE.
  apply SemWt_SemEq; eauto using ST_Suc.
  eauto using DJoin.SucCong.
Qed.

Lemma SE_App Γ i (b0 b1 a0 a1 : PTm) A B :
  Γ ⊨ PBind PPi A B ∈ (PUniv i)
  Γ ⊨ ≡ ∈ PBind PPi A B
  Γ ⊨ ≡ ∈ A
  Γ ⊨ PApp ≡ PApp ∈ subst_PTm (scons VarPTm) B.
Proof.
  move hPi.
  move /SemEq_SemWt [][]hb /SemEq_SemWt [][]ha.
  apply SemWt_SemEq; eauto using DJoin.AppCong, ST_App.
  apply : ST_Conv_E; eauto using ST_App, DJoin.cong, DJoin.symmetric, SBind_inst.
Qed.

Lemma SSu_Eq Γ (A B : PTm) i :
  Γ ⊨ A ≡ B ∈ PUniv i
  Γ ⊨ A ≲ B.
Proof. move /SemEq_SemWt h.
       qauto l:on use:SemWt_SemLEq, Sub.FromJoin.
Qed.

Lemma SSu_Transitive Γ (A B C : PTm) :
  Γ ⊨ A ≲ B
  Γ ⊨ B ≲ C
  Γ ⊨ A ≲ C.
Proof.
  move ha hb.
  apply SemLEq_SemWt in ha, hb.
  have ? : SN B by hauto l:on use:SemWt_SN.
  move : ha [ [i [ ]]]. move : hb [ [j [ ]]].
  qauto l:on use:SemWt_SemLEq, Sub.transitive.
Qed.

Lemma ST_Univ' Γ i j :
  i < j
  Γ ⊨ PUniv i ∈ PUniv j.
Proof.
  move ?.
  apply SemWt_Univ. move ρ hρ. eexists. by apply InterpUniv_Univ.
Qed.

Lemma ST_Univ Γ i :
  Γ ⊨ PUniv i ∈ PUniv (S i).
Proof.
  apply ST_Univ'. lia.
Qed.

Lemma SSu_Univ Γ i j :
  i j
  Γ ⊨ PUniv i ≲ PUniv j.
Proof.
  move h. apply : SemWt_SemLEq; eauto using ST_Univ.
  sauto lq:on.
Qed.

Lemma SSu_Pi Γ (A0 A1 : PTm ) B0 B1 :
  Γ ⊨ ≲
  cons Γ ⊨ ≲
  Γ ⊨ PBind PPi ≲ PBind PPi .
Proof.
  move hA hB.
  have ? : SN SN SN SN
    by hauto l:on use:SemLEq_SN_Sub.
  apply SemLEq_SemWt in hA, hB.
  move : hA [][i][].
  move : hB [][j][].
  apply : SemWt_SemLEq; last by hauto l:on use:Sub.PiCong.
  hauto l:on use:ST_Bind'.
  apply ST_Bind'; eauto.
  move ρ hρ.
  suff : ρ_ok (cons Γ) ρ by hauto l:on.
  move : hρ. suff : Γ_sub' ( :: Γ) ( :: Γ)
    by hauto l:on unfold:Γ_sub'.
  apply : Γ_sub'_cons; eauto. apply Γ_sub'_refl.
Qed.

Lemma SSu_Sig Γ (A0 A1 : PTm) B0 B1 :
  Γ ⊨ ≲
  cons Γ ⊨ ≲
  Γ ⊨ PBind PSig ≲ PBind PSig .
Proof.
  move hA hB.
  have ? : SN SN SN SN
    by hauto l:on use:SemLEq_SN_Sub.
  apply SemLEq_SemWt in hA, hB.
  move : hA [][i][].
  move : hB [][j][].
  apply : SemWt_SemLEq; last by hauto l:on use:Sub.SigCong.
  2 : { hauto l:on use:ST_Bind'. }
  apply ST_Bind'; eauto.
  move ρ hρ.
  suff : ρ_ok (cons Γ) ρ by hauto l:on.
  move : hρ. suff : Γ_sub' ( :: Γ) ( :: Γ) by hauto l:on.
  apply : Γ_sub'_cons; eauto.
  apply Γ_sub'_refl.
Qed.

Lemma SSu_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 :
  Γ ⊨ PBind PPi ≲ PBind PPi
  Γ ⊨ ≲ .
Proof.
  move /SemLEq_SemWt [][][]he.
  apply : SemWt_SemLEq; eauto using SBind_inv1.
  hauto lq:on rew:off use:Sub.bind_inj.
Qed.

Lemma SSu_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 :
  Γ ⊨ PBind PSig ≲ PBind PSig
  Γ ⊨ ≲ .
Proof.
  move /SemLEq_SemWt [][][]he.
  apply : SemWt_SemLEq; eauto using SBind_inv1.
  hauto lq:on rew:off use:Sub.bind_inj.
Qed.

Lemma SSu_Pi_Proj2 Γ (a0 a1 A0 A1 : PTm) B0 B1 :
  Γ ⊨ PBind PPi ≲ PBind PPi
  Γ ⊨ ≡ ∈
  Γ ⊨ subst_PTm (scons VarPTm) ≲ subst_PTm (scons VarPTm) .
Proof.
  move /SemLEq_SemWt => [/Sub.bind_inj [_ [ ]]].
  move => [i][] /SemEq_SemWt [][]ha.
  apply : SemWt_SemLEq; eauto using SBind_inst;
    last by hauto l:on use:Sub.cong.
  apply SBind_inst with (p := PPi) (A := ); eauto.
  apply : ST_Conv'; eauto. hauto l:on use:SBind_inv1.
Qed.

Lemma SSu_Sig_Proj2 Γ (a0 a1 A0 A1 : PTm) B0 B1 :
  Γ ⊨ PBind PSig ≲ PBind PSig
  Γ ⊨ ≡ ∈
  Γ ⊨ subst_PTm (scons VarPTm) ≲ subst_PTm (scons VarPTm) .
Proof.
  move /SemLEq_SemWt => [/Sub.bind_inj [_ [ ]]].
  move => [i][] /SemEq_SemWt [][]ha.
  apply : SemWt_SemLEq; eauto using SBind_inst;
    last by hauto l:on use:Sub.cong.
  apply SBind_inst with (p := PSig) (A := ); eauto.
  apply : ST_Conv'; eauto. hauto l:on use:SBind_inv1.
Qed.

Add everything to the hint database so we can solve the fundamental theorem with one application of eauto
#[export]Hint Resolve ST_Var ST_Bind ST_Abs ST_App ST_Pair ST_Proj1 ST_Proj2 ST_Univ ST_Conv
  SE_Refl SE_Symmetric SE_Transitive SE_Bind SE_Abs SE_App SE_Proj1 SE_Proj2
  SE_Conv SSu_Pi_Proj1 SSu_Pi_Proj2 SSu_Sig_Proj1 SSu_Sig_Proj2 SSu_Eq SSu_Transitive SSu_Pi SSu_Sig SemWff_nil SemWff_cons SSu_Univ SE_AppAbs SE_ProjPair1 SE_ProjPair2 SE_AppEta SE_PairEta ST_Nat ST_Ind ST_Suc ST_Zero SE_IndCong SE_SucCong SE_IndZero SE_IndSuc SE_SucCong SE_PairExt SE_FunExt : sem.