Recipes_neutralization.Recipes_neutralization
Set Warnings "-notation-overridden, -notation-overriden".
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq zify.
From Coq Require Import ssrfun PeanoNat Lia Arith_base.
Set Warnings "notation-overridden, notation-overriden".
Require Import AutosubstSsr ARS My_tactics.
Require Import Recipes.
Require Import My_autosubst.
Require Import Recipes_SN.
Require Import Recipes_NF.
Require Import Recipes_step_lemmas.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq zify.
From Coq Require Import ssrfun PeanoNat Lia Arith_base.
Set Warnings "notation-overridden, notation-overriden".
Require Import AutosubstSsr ARS My_tactics.
Require Import Recipes.
Require Import My_autosubst.
Require Import Recipes_SN.
Require Import Recipes_NF.
Require Import Recipes_step_lemmas.
The recipe r is neutral n iff its free variables are
either below n (bounded upto n) or odd.
This function make sens when applied to normal form .
Fixpoint neutral n (r : recipe) : bool :=
match r with
| Top => true
| Var h => (h < n) || odd h
| App s t
| And s t => neutral n s && neutral n t
| TApp s _
| Imp _ s
| TLam s
| TAll s => neutral n s
| Lam U s => neutral n.+2 s
end.
Lemma neutral_hsubst :
forall r θ n, neutral n r -> neutral n r.|[θ].
Proof.
elim=>//=.
{ move=> s hs t ht θ n /andP [] h1 h2.
splitb. by apply hs. by apply ht. }
{ move=> s hs t ht θ n /andP [] h1 h2.
splitb. by apply hs. by apply ht. }
{ move=> _ s hs θ n h. by apply hs. }
{ move=> s hs θ n h. by apply hs. }
{ move=> s hs θ n h. by apply hs. }
Qed.
Parameter neutral_ax : nat -> recipe -> bool.
Axiom neuneu : forall n r, neutral n r -> neutral_ax n r.
Axiom neutral_ax_and :
forall s t n,
neutral_ax n s ->
neutral_ax n t ->
neutral_ax n (And s t).
Axiom neutral_ax_imp :
forall s f n,
neutral_ax n s ->
neutral_ax n (Imp f s).
Axiom neutral_ax_tall :
forall s n,
neutral_ax n s ->
neutral_ax n (TAll s).
Axiom neutral_hsubst_ax :
forall r θ n, neutral_ax n r -> neutral_ax n r.|[θ].
match r with
| Top => true
| Var h => (h < n) || odd h
| App s t
| And s t => neutral n s && neutral n t
| TApp s _
| Imp _ s
| TLam s
| TAll s => neutral n s
| Lam U s => neutral n.+2 s
end.
Lemma neutral_hsubst :
forall r θ n, neutral n r -> neutral n r.|[θ].
Proof.
elim=>//=.
{ move=> s hs t ht θ n /andP [] h1 h2.
splitb. by apply hs. by apply ht. }
{ move=> s hs t ht θ n /andP [] h1 h2.
splitb. by apply hs. by apply ht. }
{ move=> _ s hs θ n h. by apply hs. }
{ move=> s hs θ n h. by apply hs. }
{ move=> s hs θ n h. by apply hs. }
Qed.
Parameter neutral_ax : nat -> recipe -> bool.
Axiom neuneu : forall n r, neutral n r -> neutral_ax n r.
Axiom neutral_ax_and :
forall s t n,
neutral_ax n s ->
neutral_ax n t ->
neutral_ax n (And s t).
Axiom neutral_ax_imp :
forall s f n,
neutral_ax n s ->
neutral_ax n (Imp f s).
Axiom neutral_ax_tall :
forall s n,
neutral_ax n s ->
neutral_ax n (TAll s).
Axiom neutral_hsubst_ax :
forall r θ n, neutral_ax n r -> neutral_ax n r.|[θ].
Fixpoint NEU U : cand :=
match U with
| Void => fun s => forall r, nf step s r -> neutral_ax 0 r
| Arr U V => fun s => forall t u,
conv step (App s t) u ->
NEU U t -> NEU U (neu t) ->
NEU V u
| TArr V => fun s => forall T u, conv step (TApp s T) u -> NEU V u
end.
match U with
| Void => fun s => forall r, nf step s r -> neutral_ax 0 r
| Arr U V => fun s => forall t u,
conv step (App s t) u ->
NEU U t -> NEU U (neu t) ->
NEU V u
| TArr V => fun s => forall T u, conv step (TApp s T) u -> NEU V u
end.
Definition NEUσ Γ (σ : var -> recipe) : Prop :=
forall x, NEU (Γ x) (σ x).
Lemma conv_neu U s t :
conv step s t ->
NEU U s <-> NEU U t.
Proof.
elim: U => /=.
{ move=> h; split=> h2.
{ move=> u [tu nu].
apply h2; split=>//.
apply confluent_cr in h; [|apply confluence].
destruct h as [u' hu'].
have [z hz hz2]: joinable (star step) u' u.
by apply confluence with t.
have->: u = z by apply (normal_star (e:=step)).
by apply star_trans with u'. }
{ move=> u [su nu].
apply h2; split=>//.
apply confluent_cr in h; [|apply confluence].
destruct h as [u' hu'].
have [z hz hz2]: joinable (star step) u' u.
by apply confluence with s.
have->: u = z by apply (normal_star (e:=step)).
by apply star_trans with u'. } }
{ move=> U hU V hV hconv; split => h u v hconv2 hu hnu.
{ apply (h u)=>//{hU hV hu hnu h}.
apply conv_trans with (App t u) => //.
apply: (conv_hom (App^~ u) step)=>//.
by constructor. }
{ apply (h u)=>//{hU hV hu hnu h}.
apply conv_trans with (App s u) => //.
apply: (conv_hom (App^~ u) step)=>//.
by constructor.
by apply conv_sym. } }
{ move=> V hV hconv; split => h T u hconv2.
{ apply h with T => //.
apply conv_trans with (TApp t T)=>//.
apply: (conv_hom (TApp^~ T) step)=>//.
by constructor. }
{ apply h with T => //.
apply conv_trans with (TApp s T)=>//.
apply: (conv_hom (TApp^~ T) step)=>//.
by constructor.
by apply conv_sym. } }
Qed.
Corollary step_neu U s t :
step s t -> NEU U s <-> NEU U t.
Proof.
move=> h.
apply conv1 in h.
by apply conv_neu.
Qed.
Corollary step_neu_1 U s t :
step s t -> NEU U s -> NEU U t.
Proof. by apply step_neu. Qed.
Corollary step_neu_2 U s t :
step s t -> NEU U t -> NEU U s.
Proof. by apply step_neu. Qed.
Corollary nf_neu U s t :
nf step s t ->
NEU U s <-> NEU U t.
Proof.
move=>[h1 h2].
apply star_conv in h1.
by apply conv_neu.
Qed.
Corollary nf_neu_1 U s t :
nf step s t -> NEU U s -> NEU U t.
Proof. by apply nf_neu. Qed.
Corollary nf_neu_2 U s t :
nf step s t -> NEU U t -> NEU U s.
Proof. by apply nf_neu. Qed.
Lemma neu_hsubst s U θ: NEU U s -> NEU U s.|[θ].
Proof.
elim: U s θ.
{ move=> s θ /= h rθ hrθ.
destruct (inv_nf_hsubst _ _ _ hrθ) as [r [hr hr2]].
subst.
(* BEGIN AX *)
by apply neutral_hsubst_ax, h.
(* END AX *)
}
{ move=> U hU V hV s θ /= h t u hconv ht hnt.
apply (conv_neu V) in hconv.
apply hconv=>{hconv u}.
have[n hn]:= choose_last_n_hsubst s.
set r := t.|[ren (+n)].
set θθ := fun i => if i < n then θ i else TVar (i-n).
have hsr: NEU V (App s r).
{ apply h with r.
+ by constructor.
+ by apply hU.
+ rewrite /r neutralize_comm_subst_corr_hsubst.
by apply hU. }
specialize (hV (App s r) θθ hsr).
have eq: s.|[θθ] = s.|[θ] by rewrite free_above_n.
have eq2: r.|[θθ] = t.
{ rewrite/θθ/r/=.
asimpl.
unfold ">>>".
have->:
t.|[fun x : var => if eqn (((+n) x).+1 - n) 0 then θ ((+n) x) else TVar ((+n) x - n)] =
t.|[fun x : var => if eqn x.+1 0 then θ ((+n) x) else TVar ((+n) x - n)].
{ have e: forall x, (((+n) x).+1 - n) = x.+1 by asimpl; lia.
f_equal; f_ext=> x.
by rewrite e. }
simpl.
have->: t.|[fun x : var => TVar ((n + x)%coq_nat - n)] = t.|[fun x : var => TVar x]
by f_equal; f_ext => x; f_equal; lia.
have e: (fun x => TVar x) = ids by autosubst.
rewrite e.
by autosubst. }
simpl in hV.
by congruence. }
{ move=> U hU s θ h /= T u hconv.
apply (conv_neu U) in hconv.
apply hconv=>{hconv u}.
have[n hn]:= choose_last_n_hsubst s.
set R := T.[ren (+n)].
set θθ := fun i => if i < n then θ i else TVar (i-n).
have hsr: NEU U (TApp s R). apply h with R. by constructor.
specialize (hU (TApp s R) θθ hsr).
have eq: s.|[θθ] = s.|[θ] by rewrite free_above_n.
have eq2: R.[θθ] = T.
{ rewrite/θθ/R; asimpl.
have->:
T.[fun x : var => if eqn (((+n) x).+1 - n) 0 then θ ((+n) x) else TVar ((+n) x - n)] =
T.[fun x : var => if eqn x.+1 0 then θ ((+n) x) else TVar ((+n) x - n)].
{ have e: forall x, (((+n) x).+1 - n) = x.+1 by asimpl; lia.
f_equal; f_ext=> x.
by rewrite e. }
simpl.
have->: T.[fun x : var => TVar ((n + x)%coq_nat - n)] = T.[fun x : var => TVar x]
by f_equal; f_ext => x; f_equal; lia.
have e: (fun x => TVar x) = ids by autosubst.
rewrite e.
by autosubst. }
simpl in hU.
by congruence. }
Qed.
forall x, NEU (Γ x) (σ x).
Lemma conv_neu U s t :
conv step s t ->
NEU U s <-> NEU U t.
Proof.
elim: U => /=.
{ move=> h; split=> h2.
{ move=> u [tu nu].
apply h2; split=>//.
apply confluent_cr in h; [|apply confluence].
destruct h as [u' hu'].
have [z hz hz2]: joinable (star step) u' u.
by apply confluence with t.
have->: u = z by apply (normal_star (e:=step)).
by apply star_trans with u'. }
{ move=> u [su nu].
apply h2; split=>//.
apply confluent_cr in h; [|apply confluence].
destruct h as [u' hu'].
have [z hz hz2]: joinable (star step) u' u.
by apply confluence with s.
have->: u = z by apply (normal_star (e:=step)).
by apply star_trans with u'. } }
{ move=> U hU V hV hconv; split => h u v hconv2 hu hnu.
{ apply (h u)=>//{hU hV hu hnu h}.
apply conv_trans with (App t u) => //.
apply: (conv_hom (App^~ u) step)=>//.
by constructor. }
{ apply (h u)=>//{hU hV hu hnu h}.
apply conv_trans with (App s u) => //.
apply: (conv_hom (App^~ u) step)=>//.
by constructor.
by apply conv_sym. } }
{ move=> V hV hconv; split => h T u hconv2.
{ apply h with T => //.
apply conv_trans with (TApp t T)=>//.
apply: (conv_hom (TApp^~ T) step)=>//.
by constructor. }
{ apply h with T => //.
apply conv_trans with (TApp s T)=>//.
apply: (conv_hom (TApp^~ T) step)=>//.
by constructor.
by apply conv_sym. } }
Qed.
Corollary step_neu U s t :
step s t -> NEU U s <-> NEU U t.
Proof.
move=> h.
apply conv1 in h.
by apply conv_neu.
Qed.
Corollary step_neu_1 U s t :
step s t -> NEU U s -> NEU U t.
Proof. by apply step_neu. Qed.
Corollary step_neu_2 U s t :
step s t -> NEU U t -> NEU U s.
Proof. by apply step_neu. Qed.
Corollary nf_neu U s t :
nf step s t ->
NEU U s <-> NEU U t.
Proof.
move=>[h1 h2].
apply star_conv in h1.
by apply conv_neu.
Qed.
Corollary nf_neu_1 U s t :
nf step s t -> NEU U s -> NEU U t.
Proof. by apply nf_neu. Qed.
Corollary nf_neu_2 U s t :
nf step s t -> NEU U t -> NEU U s.
Proof. by apply nf_neu. Qed.
Lemma neu_hsubst s U θ: NEU U s -> NEU U s.|[θ].
Proof.
elim: U s θ.
{ move=> s θ /= h rθ hrθ.
destruct (inv_nf_hsubst _ _ _ hrθ) as [r [hr hr2]].
subst.
(* BEGIN AX *)
by apply neutral_hsubst_ax, h.
(* END AX *)
}
{ move=> U hU V hV s θ /= h t u hconv ht hnt.
apply (conv_neu V) in hconv.
apply hconv=>{hconv u}.
have[n hn]:= choose_last_n_hsubst s.
set r := t.|[ren (+n)].
set θθ := fun i => if i < n then θ i else TVar (i-n).
have hsr: NEU V (App s r).
{ apply h with r.
+ by constructor.
+ by apply hU.
+ rewrite /r neutralize_comm_subst_corr_hsubst.
by apply hU. }
specialize (hV (App s r) θθ hsr).
have eq: s.|[θθ] = s.|[θ] by rewrite free_above_n.
have eq2: r.|[θθ] = t.
{ rewrite/θθ/r/=.
asimpl.
unfold ">>>".
have->:
t.|[fun x : var => if eqn (((+n) x).+1 - n) 0 then θ ((+n) x) else TVar ((+n) x - n)] =
t.|[fun x : var => if eqn x.+1 0 then θ ((+n) x) else TVar ((+n) x - n)].
{ have e: forall x, (((+n) x).+1 - n) = x.+1 by asimpl; lia.
f_equal; f_ext=> x.
by rewrite e. }
simpl.
have->: t.|[fun x : var => TVar ((n + x)%coq_nat - n)] = t.|[fun x : var => TVar x]
by f_equal; f_ext => x; f_equal; lia.
have e: (fun x => TVar x) = ids by autosubst.
rewrite e.
by autosubst. }
simpl in hV.
by congruence. }
{ move=> U hU s θ h /= T u hconv.
apply (conv_neu U) in hconv.
apply hconv=>{hconv u}.
have[n hn]:= choose_last_n_hsubst s.
set R := T.[ren (+n)].
set θθ := fun i => if i < n then θ i else TVar (i-n).
have hsr: NEU U (TApp s R). apply h with R. by constructor.
specialize (hU (TApp s R) θθ hsr).
have eq: s.|[θθ] = s.|[θ] by rewrite free_above_n.
have eq2: R.[θθ] = T.
{ rewrite/θθ/R; asimpl.
have->:
T.[fun x : var => if eqn (((+n) x).+1 - n) 0 then θ ((+n) x) else TVar ((+n) x - n)] =
T.[fun x : var => if eqn x.+1 0 then θ ((+n) x) else TVar ((+n) x - n)].
{ have e: forall x, (((+n) x).+1 - n) = x.+1 by asimpl; lia.
f_equal; f_ext=> x.
by rewrite e. }
simpl.
have->: T.[fun x : var => TVar ((n + x)%coq_nat - n)] = T.[fun x : var => TVar x]
by f_equal; f_ext => x; f_equal; lia.
have e: (fun x => TVar x) = ids by autosubst.
rewrite e.
by autosubst. }
simpl in hU.
by congruence. }
Qed.
Theorem neutralization_soundness [Γ : ctx] [U : type] (s : recipe):
[ Γ ⊢ ] -> [ Γ ⊢ s :- U ] ->
forall σ θ, admissible_subst σ -> NEUσ Γ σ ->
NEU U s.|[θ].[σ].
Proof.
elim: s U Γ.
(* {Case Top} *)
{ move=> U Γ wf wt σ θ ad el /=.
inv wt=> /= r nr.
(* BEGIN AX *)
apply neuneu.
(* END AX *)
by rewrite (nf_top_is_top _ nr) /neu/sneu/=/neutral/=. }
(* {Case Var} *)
{ move=> v U Γ wf wt σ θ ad el.
inv wt.
by apply el. }
(* {Case App} *)
{ move=> s hs t ht U Γ wf wt σ θ ad el.
asimpl.
inv wt.
specialize (hs (Arr U0 U) Γ wf H1 σ θ ad el).
have ht₀ := (ht U0 Γ wf H3 σ θ ad el).
simpl in hs.
apply hs with t.|[θ].[σ] => //.
have->: (neu t.|[θ].[σ]) = t.|[θ].[σ >> sneu] by rewrite /neu/sneu/ns; asimpl.
have ht1:= (ht U0 Γ wf H3 (σ >> sneu) θ).
apply ht1.
+ by apply admissible_compose, admissible_neu.
+ move=>{hs ht H1 H3 ht1 ht₀ θ U0 U t} x.
(* TODO simplifier *)
case (boolP (odd x))=> [o|no].
{ asimpl.
simpl in ad.
have xisx: x.-1.+1 = x by lia.
have had: ~~ odd x.-1 by lia.
specialize (ad x.-1 had)=>{had}.
rewrite xisx in ad.
rewrite ad.
have->: (neu (σ x.-1)).[sneu] = neu (neu (σ x.-1)) by done.
rewrite -neu_idempotent.
by rewrite -ad. }
{ have no2: odd x.+1 by lia.
have->:((σ>>sneu) x) = neu (σ x) by autosubst.
rewrite -(ad x no2).
have->: Γ x = Γ x.+1 by rewrite wf.
exact: el. } }
(* {Case And} *)
{ move=> s hs t ht U Γ wf wt σ θ ad el.
inv wt=> u /= [hu1 hu2].
have[ss [tt [eu [h1 h2]]]]:= red_and_inv s.|[θ].[σ] t.|[θ].[σ] u hu1.
rewrite eu in hu2, hu1.
have [hns hnt]:= normande ss tt hu2.
rewrite eu=>/=.
(* BEGIN AX *)
apply neutral_ax_and.
simpl in hs.
(* END AX *)
by apply (hs Void Γ wf H1 σ θ ad el).
by apply (ht Void Γ wf H3 σ θ ad el). }
(* {Case TApp} *)
{ move=> s hs S U Γ wf wt σ θ ad el.
inv wt=>/=.
specialize (hs (TArr U) Γ wf H2 σ θ ad el).
simpl in hs.
specialize (hs S.[θ] (TApp s.|[θ].[σ] S.[θ])).
by apply hs. }
(* {Case Imp} *)
{ move=> f s hs U Γ wf wt σ θ ad el.
inv wt=>/= u [hu1 hu2].
specialize (hs Void Γ wf H2 σ θ ad el).
simpl in hs.
destruct (red_imp_inv _ _ _ hu1) as [w [h1 h2]].
subst.
(* BEGIN AX *)
apply neutral_ax_imp.
(* END AX *)
apply hs.
split=>//.
by apply (normimp f). }
(* {Case Lam} *)
{ move=> U s hs V Γ wf wt σ θ ad el.
inv wt=> /= t u hconv ht hnt.
have hconv2 : conv step s.|[θ].[t .: neu t .: σ] u.
apply conv_trans with (App (Lam U s.|[θ].[upn 2 σ]) t)=>//.
apply conv_sym, conv1, step_beta.
autosubst.
apply (conv_neu V0) in hconv2.
apply hconv2.
apply hs with (U .: U .: Γ) => //.
+ by apply wf_ext.
+ by apply admissible_subst_ext.
+ rewrite/NEUσ.
case=>//=.
case=>//=. }
(* {Case TLam} *)
{ move=> s hs U Γ wf wt σ θ ad el.
inv wt=> /= T u hconv.
set t := s.|[T .: θ].[σ].
have hconv2: conv step u t.
{ apply conv_trans with (TApp (TLam s.|[up θ].[σ >>| ren (+1)]) T).
by apply conv_sym.
apply conv1.
constructor.
by asimpl. }
apply (conv_neu U0) in hconv2.
apply hconv2.
apply hs with Γ=>//. }
(* {Case TAll} *)
{ move=> s hs U Γ wf wt σ θ ad el.
set σ1 := (σ >>| ren (+1)) .
inv wt=> /= u [hu1 hu2].
fold σ1 in hu1.
have ad1 : admissible_subst σ1 by apply admissible_hsubst.
have el1: NEUσ Γ σ1.
{ move=>v.
rewrite/σ1.
have->: (σ >>| ren (+1)) v = (σ v).|[ren (+1)] by autosubst.
rewrite /admissible_subst in ad.
specialize (el v).
by apply neu_hsubst. }
specialize (hs Void _ wf H0 σ1 (up θ) ad1).
simpl in hs.
destruct (red_tall_inv _ _ hu1) as [w [h1 h2]].
subst.
have {h2 hu2}nfw: nf step s.|[up θ].[σ1] w by split; [done| apply normall].
(* BEGIN AX *)
apply neutral_ax_tall.
(* END AX *)
by apply hs. }
Qed.
(* Print Assumptions neutralization_soundness. *)
[ Γ ⊢ ] -> [ Γ ⊢ s :- U ] ->
forall σ θ, admissible_subst σ -> NEUσ Γ σ ->
NEU U s.|[θ].[σ].
Proof.
elim: s U Γ.
(* {Case Top} *)
{ move=> U Γ wf wt σ θ ad el /=.
inv wt=> /= r nr.
(* BEGIN AX *)
apply neuneu.
(* END AX *)
by rewrite (nf_top_is_top _ nr) /neu/sneu/=/neutral/=. }
(* {Case Var} *)
{ move=> v U Γ wf wt σ θ ad el.
inv wt.
by apply el. }
(* {Case App} *)
{ move=> s hs t ht U Γ wf wt σ θ ad el.
asimpl.
inv wt.
specialize (hs (Arr U0 U) Γ wf H1 σ θ ad el).
have ht₀ := (ht U0 Γ wf H3 σ θ ad el).
simpl in hs.
apply hs with t.|[θ].[σ] => //.
have->: (neu t.|[θ].[σ]) = t.|[θ].[σ >> sneu] by rewrite /neu/sneu/ns; asimpl.
have ht1:= (ht U0 Γ wf H3 (σ >> sneu) θ).
apply ht1.
+ by apply admissible_compose, admissible_neu.
+ move=>{hs ht H1 H3 ht1 ht₀ θ U0 U t} x.
(* TODO simplifier *)
case (boolP (odd x))=> [o|no].
{ asimpl.
simpl in ad.
have xisx: x.-1.+1 = x by lia.
have had: ~~ odd x.-1 by lia.
specialize (ad x.-1 had)=>{had}.
rewrite xisx in ad.
rewrite ad.
have->: (neu (σ x.-1)).[sneu] = neu (neu (σ x.-1)) by done.
rewrite -neu_idempotent.
by rewrite -ad. }
{ have no2: odd x.+1 by lia.
have->:((σ>>sneu) x) = neu (σ x) by autosubst.
rewrite -(ad x no2).
have->: Γ x = Γ x.+1 by rewrite wf.
exact: el. } }
(* {Case And} *)
{ move=> s hs t ht U Γ wf wt σ θ ad el.
inv wt=> u /= [hu1 hu2].
have[ss [tt [eu [h1 h2]]]]:= red_and_inv s.|[θ].[σ] t.|[θ].[σ] u hu1.
rewrite eu in hu2, hu1.
have [hns hnt]:= normande ss tt hu2.
rewrite eu=>/=.
(* BEGIN AX *)
apply neutral_ax_and.
simpl in hs.
(* END AX *)
by apply (hs Void Γ wf H1 σ θ ad el).
by apply (ht Void Γ wf H3 σ θ ad el). }
(* {Case TApp} *)
{ move=> s hs S U Γ wf wt σ θ ad el.
inv wt=>/=.
specialize (hs (TArr U) Γ wf H2 σ θ ad el).
simpl in hs.
specialize (hs S.[θ] (TApp s.|[θ].[σ] S.[θ])).
by apply hs. }
(* {Case Imp} *)
{ move=> f s hs U Γ wf wt σ θ ad el.
inv wt=>/= u [hu1 hu2].
specialize (hs Void Γ wf H2 σ θ ad el).
simpl in hs.
destruct (red_imp_inv _ _ _ hu1) as [w [h1 h2]].
subst.
(* BEGIN AX *)
apply neutral_ax_imp.
(* END AX *)
apply hs.
split=>//.
by apply (normimp f). }
(* {Case Lam} *)
{ move=> U s hs V Γ wf wt σ θ ad el.
inv wt=> /= t u hconv ht hnt.
have hconv2 : conv step s.|[θ].[t .: neu t .: σ] u.
apply conv_trans with (App (Lam U s.|[θ].[upn 2 σ]) t)=>//.
apply conv_sym, conv1, step_beta.
autosubst.
apply (conv_neu V0) in hconv2.
apply hconv2.
apply hs with (U .: U .: Γ) => //.
+ by apply wf_ext.
+ by apply admissible_subst_ext.
+ rewrite/NEUσ.
case=>//=.
case=>//=. }
(* {Case TLam} *)
{ move=> s hs U Γ wf wt σ θ ad el.
inv wt=> /= T u hconv.
set t := s.|[T .: θ].[σ].
have hconv2: conv step u t.
{ apply conv_trans with (TApp (TLam s.|[up θ].[σ >>| ren (+1)]) T).
by apply conv_sym.
apply conv1.
constructor.
by asimpl. }
apply (conv_neu U0) in hconv2.
apply hconv2.
apply hs with Γ=>//. }
(* {Case TAll} *)
{ move=> s hs U Γ wf wt σ θ ad el.
set σ1 := (σ >>| ren (+1)) .
inv wt=> /= u [hu1 hu2].
fold σ1 in hu1.
have ad1 : admissible_subst σ1 by apply admissible_hsubst.
have el1: NEUσ Γ σ1.
{ move=>v.
rewrite/σ1.
have->: (σ >>| ren (+1)) v = (σ v).|[ren (+1)] by autosubst.
rewrite /admissible_subst in ad.
specialize (el v).
by apply neu_hsubst. }
specialize (hs Void _ wf H0 σ1 (up θ) ad1).
simpl in hs.
destruct (red_tall_inv _ _ hu1) as [w [h1 h2]].
subst.
have {h2 hu2}nfw: nf step s.|[up θ].[σ1] w by split; [done| apply normall].
(* BEGIN AX *)
apply neutral_ax_tall.
(* END AX *)
by apply hs. }
Qed.
(* Print Assumptions neutralization_soundness. *)