Theorem: Lean4Lean.ConditionallyTyped.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 : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
⊢ ConditionallyTyped ngen env Us Δ e
Tactic:
refine H.imp_right fun H1 H2 => ?_
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
H1 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → ∃ e', TrExpr env Us ((some fv, d) :: Δ) e e'
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
⊢ ∃ e', TrExpr env Us Δ e e'

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
H1 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → ∃ e', TrExpr env Us ((some fv, d) :: Δ) e e'
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
⊢ ∃ e', TrExpr env Us Δ e e'
Tactic:
have ⟨e', H⟩ := H1 H2.fvars_cons
State after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H✝ : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
H1 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → ∃ e', TrExpr env Us ((some fv, d) :: Δ) e e'
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
e' : VExpr
H : TrExpr env Us ((some fv, d) :: Δ) e e'
⊢ ∃ e', TrExpr env Us Δ e e'

State before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H✝ : ConditionallyTyped ngen env Us ((some fv, d) :: Δ) e
H1 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → ∃ e', TrExpr env Us ((some fv, d) :: Δ) e e'
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
e' : VExpr
H : TrExpr env Us ((some fv, d) :: Δ) e e'
⊢ ∃ e', TrExpr env Us Δ e e'
Tactic:
exact TrExpr.weakN_inv henv (.skip_fvar _ _ .refl) (.refl henv hΔ) H H2
State after:
no goals