Theorem: Lean4Lean.ConditionallyHasType.weakN_inv (Lean4Lean/Verify/Typing/ConditionallyTyped.lean)

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
⊢ ConditionallyHasType ngen env Us Δ e A
Tactic:
have ⟨H1, H2, H3⟩ := H
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
⊢ ConditionallyHasType ngen env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
⊢ ConditionallyHasType ngen env Us Δ e A
Tactic:
refine ⟨H1, H2, fun H4 => ?_⟩
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
⊢ TrHasType env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
⊢ TrHasType env Us Δ e A
Tactic:
have ⟨h1, e', A', h2, h3, h4⟩ := H3 H4.fvars_cons
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
⊢ TrHasType env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
⊢ TrHasType env Us Δ e A
Tactic:
have W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + d.depth) 0 := .skip_fvar _ _ .refl
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ TrHasType env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ TrHasType env Us Δ e A
Tactic:
have ⟨e'', he⟩ := TrExpr.weakN_inv henv W (.refl henv hΔ) h2 H4
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
⊢ TrHasType env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
⊢ TrHasType env Us Δ e A
Tactic:
have ee := h2.uniq henv (.refl henv hΔ) <| he.weakN henv W hΔ
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
⊢ TrHasType env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
⊢ TrHasType env Us Δ e A
Tactic:
have ⟨_, hA⟩ := TrExpr.weakN_inv henv W (.refl henv hΔ) h3 <| h1 _ this H4
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
⊢ TrHasType env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
⊢ TrHasType env Us Δ e A
Tactic:
have AA := h3.uniq henv (.refl henv hΔ) <| hA.weakN henv W hΔ
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
⊢ TrHasType env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
⊢ TrHasType env Us Δ e A
Tactic:
have h4 := h4.defeqU_r henv hΔ.toCtx AA |>.defeqU_l henv hΔ.toCtx ee
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
⊢ TrHasType env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
⊢ TrHasType env Us Δ e A
Tactic:
have h4 := (HasType.weakN_iff henv hΔ.toCtx W.toCtx).1 h4
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝¹ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4✝ :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) e'' w✝
⊢ TrHasType env Us Δ e A

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝¹ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4✝ :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) e'' w✝
⊢ TrHasType env Us Δ e A
Tactic:
refine ⟨fun P hP he' => ?_, _, _, he, hA, h4⟩
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝¹ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4✝ :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) e'' w✝
P : FVarId → Prop
hP : IsFVarUpSet P Δ
he' : InScope P e
⊢ InScope P A