Theorem: Lean4Lean.ConditionallyTyped.fresh (Lean4Lean/Verify/Typing/ConditionallyTyped.lean)

State before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
⊢ ConditionallyTyped ngen env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e
Tactic:
refine have ⟨H1, H2⟩ := H; ⟨H1, fun H3 => ?_⟩
State after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∃ e', TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e e'

State before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∃ e', TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e e'
Tactic:
refine have ⟨_, h⟩ := H2 (H3.mp ?_ H1); ⟨_, h.weakN henv (.skip_fvar _ _ .refl) hΔ⟩
State after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∀ (fv : FVarId),
    fv ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ) →
      NameGenerator.Reserves ngen fv → fv ∈ VLCtx.fvars Δ

State before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∀ (fv : FVarId),
    fv ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ) →
      NameGenerator.Reserves ngen fv → fv ∈ VLCtx.fvars Δ
Tactic:
intro _ h1 h2
State after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h1 : fv✝ ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)
h2 : NameGenerator.Reserves ngen fv✝
⊢ fv✝ ∈ VLCtx.fvars Δ

State before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h1 : fv✝ ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)
h2 : NameGenerator.Reserves ngen fv✝
⊢ fv✝ ∈ VLCtx.fvars Δ
Tactic:
simp at h1
State after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ = { name := NameGenerator.curr ngen } ∨ fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ

State before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ = { name := NameGenerator.curr ngen } ∨ fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ
Tactic:
rcases h1 with rfl | h1
State after:
case inl
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h2 : NameGenerator.Reserves ngen { name := NameGenerator.curr ngen }
⊢ { name := NameGenerator.curr ngen } ∈ VLCtx.fvars Δ

case inr
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ

State before:
case inl
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h2 : NameGenerator.Reserves ngen { name := NameGenerator.curr ngen }
⊢ { name := NameGenerator.curr ngen } ∈ VLCtx.fvars Δ
Tactic:
cases Nat.lt_irrefl _ (h2 _ rfl)
State after:
no goals

State before:
case inr
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyTyped ngen env Us Δ e
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → ∃ e', TrExpr env Us Δ e e'
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ
Tactic:
exact h1
State after:
no goals