Theorem: Lean4Lean.VEnv.IsDefEq.closedN' (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
hΓ : CtxClosed Γ
⊢ ClosedN e1 (List.length Γ) ∧ ClosedN e2 (List.length Γ) ∧ ClosedN A (List.length Γ)
Tactic:
induction H with
| bvar h => exact ⟨h.lt, h.lt, hΓ.lookup h⟩
| constDF h1 =>
  let ⟨_, h, _⟩ := henv.1 h1
  exact ⟨trivial, trivial, h.instL.mono (Nat.zero_le _)⟩
| sortDF => exact ⟨trivial, trivial, trivial⟩
| symm _ ih => let ⟨h1, h2, h3⟩ := ih hΓ; exact ⟨h2, h1, h3⟩
| trans _ _ ih1 ih2 => exact ⟨(ih1 hΓ).1, (ih2 hΓ).2.1, (ih1 hΓ).2.2⟩
| appDF _ _ ih1 ih2 =>
  let ⟨hf, hf', _, hB⟩ := ih1 hΓ
  let ⟨ha, ha', _⟩ := ih2 hΓ
  exact ⟨⟨hf, ha⟩, ⟨hf', ha'⟩, hB.inst ha⟩
| lamDF _ _ ih1 ih2 =>
  let ⟨hA, hA', _⟩ := ih1 hΓ
  let ⟨hb, hb', hB⟩ := ih2 ⟨hΓ, hA⟩
  exact ⟨⟨hA, hb⟩, ⟨hA', hb'⟩, hA, hB⟩
| forallEDF _ _ ih1 ih2 =>
  let ⟨hA, hA', _⟩ := ih1 hΓ
  let ⟨hb, hb', _⟩ := ih2 ⟨hΓ, hA⟩
  exact ⟨⟨hA, hb⟩, ⟨hA', hb'⟩, trivial⟩
| defeqDF _ _ ih1 ih2 => exact ⟨(ih2 hΓ).1, (ih2 hΓ).2.1, (ih1 hΓ).2.1⟩
| beta _ _ ih1 ih2 =>
  let ⟨he', _, hA⟩ := ih2 hΓ
  let ⟨he, _, hB⟩ := ih1 ⟨hΓ, hA⟩
  exact ⟨⟨⟨hA, he⟩, he'⟩, he.inst he', hB.inst he'⟩
| eta _ ih =>
  let ⟨he, _, hA, hB⟩ := ih hΓ
  exact ⟨⟨hA, he.liftN, Nat.succ_pos _⟩, he, hA, hB⟩
| proofIrrel _ _ _ _ ih2 ih3 =>
  let ⟨hh, _, _⟩ := ih2 hΓ
  let ⟨hh', _, hp⟩ := ih3 hΓ
  exact ⟨hh, hh', hp⟩
| extra h1 _ _ =>
  let ⟨⟨hl, _⟩, ⟨hr, hA⟩⟩ := henv.2 h1
  exact ⟨
    hl.instL.mono (Nat.zero_le _),
    hr.instL.mono (Nat.zero_le _),
    hA.instL.mono (Nat.zero_le _)⟩
State after:
no goals

State before:
case bvar
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
hΓ : CtxClosed Γ✝
⊢ ClosedN (VExpr.bvar i✝) (List.length Γ✝) ∧ ClosedN (VExpr.bvar i✝) (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
Tactic:
exact ⟨h.lt, h.lt, hΓ.lookup h⟩
State after:
no goals

State before:
case constDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
a✝³ : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝² : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝¹ : List.length ls✝ = ci✝.uvars
a✝ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
hΓ : CtxClosed Γ✝
⊢ ClosedN (VExpr.const c✝ ls✝) (List.length Γ✝) ∧
    ClosedN (VExpr.const c✝ ls'✝) (List.length Γ✝) ∧ ClosedN (instL ls✝ ci✝.type) (List.length Γ✝)
Tactic:
let ⟨_, h, _⟩ := henv.1 h1
State after:
case constDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
a✝³ : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝² : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝¹ : List.length ls✝ = ci✝.uvars
a✝ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
hΓ : CtxClosed Γ✝
w✝ : VLevel
h : ClosedN ci✝.type
right✝ : ClosedN (VExpr.sort w✝)
⊢ ClosedN (VExpr.const c✝ ls✝) (List.length Γ✝) ∧
    ClosedN (VExpr.const c✝ ls'✝) (List.length Γ✝) ∧ ClosedN (instL ls✝ ci✝.type) (List.length Γ✝)

State before:
case constDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
a✝³ : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝² : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝¹ : List.length ls✝ = ci✝.uvars
a✝ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
hΓ : CtxClosed Γ✝
w✝ : VLevel
h : ClosedN ci✝.type
right✝ : ClosedN (VExpr.sort w✝)
⊢ ClosedN (VExpr.const c✝ ls✝) (List.length Γ✝) ∧
    ClosedN (VExpr.const c✝ ls'✝) (List.length Γ✝) ∧ ClosedN (instL ls✝ ci✝.type) (List.length Γ✝)
Tactic:
exact ⟨trivial, trivial, h.instL.mono (Nat.zero_le _)⟩
State after:
no goals

State before:
case sortDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
a✝² : VLevel.WF U l✝
a✝¹ : VLevel.WF U l'✝
a✝ : l✝ ≈ l'✝
hΓ : CtxClosed Γ✝
⊢ ClosedN (VExpr.sort l✝) (List.length Γ✝) ∧
    ClosedN (VExpr.sort l'✝) (List.length Γ✝) ∧ ClosedN (VExpr.sort (VLevel.succ l✝)) (List.length Γ✝)
Tactic:
exact ⟨trivial, trivial, trivial⟩
State after:
no goals

State before:
case symm
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : CtxClosed Γ✝ → ClosedN e✝ (List.length Γ✝) ∧ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
⊢ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN e✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
Tactic:
let ⟨h1, h2, h3⟩ := ih hΓ
State after:
case symm
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : CtxClosed Γ✝ → ClosedN e✝ (List.length Γ✝) ∧ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
h1 : ClosedN e✝ (List.length Γ✝)
h2 : ClosedN e'✝ (List.length Γ✝)
h3 : ClosedN A✝ (List.length Γ✝)
⊢ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN e✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)

State before:
case symm
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : CtxClosed Γ✝ → ClosedN e✝ (List.length Γ✝) ∧ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
h1 : ClosedN e✝ (List.length Γ✝)
h2 : ClosedN e'✝ (List.length Γ✝)
h3 : ClosedN A✝ (List.length Γ✝)
⊢ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN e✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
Tactic:
exact ⟨h2, h1, h3⟩
State after:
no goals

State before:
case trans
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEq env U Γ✝ e₂✝ e₃✝ A✝
ih1 : CtxClosed Γ✝ → ClosedN e₁✝ (List.length Γ✝) ∧ ClosedN e₂✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN e₂✝ (List.length Γ✝) ∧ ClosedN e₃✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
⊢ ClosedN e₁✝ (List.length Γ✝) ∧ ClosedN e₃✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
Tactic:
exact ⟨(ih1 hΓ).1, (ih2 hΓ).2.1, (ih1 hΓ).2.2⟩
State after:
no goals

State before:
case appDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 :
  CtxClosed Γ✝ →
    ClosedN f✝ (List.length Γ✝) ∧ ClosedN f'✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN a✝² (List.length Γ✝) ∧ ClosedN a'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
⊢ ClosedN (app f✝ a✝²) (List.length Γ✝) ∧
    ClosedN (app f'✝ a'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ a✝²) (List.length Γ✝)
Tactic:
let ⟨hf, hf', _, hB⟩ := ih1 hΓ
State after:
case appDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 :
  CtxClosed Γ✝ →
    ClosedN f✝ (List.length Γ✝) ∧ ClosedN f'✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN a✝² (List.length Γ✝) ∧ ClosedN a'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
hf : ClosedN f✝ (List.length Γ✝)
hf' : ClosedN f'✝ (List.length Γ✝)
left✝ : ClosedN A✝ (List.length Γ✝)
hB : ClosedN B✝ (List.length Γ✝ + 1)
⊢ ClosedN (app f✝ a✝²) (List.length Γ✝) ∧
    ClosedN (app f'✝ a'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ a✝²) (List.length Γ✝)

State before:
case appDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 :
  CtxClosed Γ✝ →
    ClosedN f✝ (List.length Γ✝) ∧ ClosedN f'✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN a✝² (List.length Γ✝) ∧ ClosedN a'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
hf : ClosedN f✝ (List.length Γ✝)
hf' : ClosedN f'✝ (List.length Γ✝)
left✝ : ClosedN A✝ (List.length Γ✝)
hB : ClosedN B✝ (List.length Γ✝ + 1)
⊢ ClosedN (app f✝ a✝²) (List.length Γ✝) ∧
    ClosedN (app f'✝ a'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ a✝²) (List.length Γ✝)
Tactic:
let ⟨ha, ha', _⟩ := ih2 hΓ
State after:
case appDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 :
  CtxClosed Γ✝ →
    ClosedN f✝ (List.length Γ✝) ∧ ClosedN f'✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN a✝² (List.length Γ✝) ∧ ClosedN a'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
hf : ClosedN f✝ (List.length Γ✝)
hf' : ClosedN f'✝ (List.length Γ✝)
left✝ : ClosedN A✝ (List.length Γ✝)
hB : ClosedN B✝ (List.length Γ✝ + 1)
ha : ClosedN a✝² (List.length Γ✝)
ha' : ClosedN a'✝ (List.length Γ✝)
right✝ : ClosedN A✝ (List.length Γ✝)
⊢ ClosedN (app f✝ a✝²) (List.length Γ✝) ∧
    ClosedN (app f'✝ a'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ a✝²) (List.length Γ✝)

State before:
case appDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 :
  CtxClosed Γ✝ →
    ClosedN f✝ (List.length Γ✝) ∧ ClosedN f'✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN a✝² (List.length Γ✝) ∧ ClosedN a'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
hf : ClosedN f✝ (List.length Γ✝)
hf' : ClosedN f'✝ (List.length Γ✝)
left✝ : ClosedN A✝ (List.length Γ✝)
hB : ClosedN B✝ (List.length Γ✝ + 1)
ha : ClosedN a✝² (List.length Γ✝)
ha' : ClosedN a'✝ (List.length Γ✝)
right✝ : ClosedN A✝ (List.length Γ✝)
⊢ ClosedN (app f✝ a✝²) (List.length Γ✝) ∧
    ClosedN (app f'✝ a'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ a✝²) (List.length Γ✝)
Tactic:
exact ⟨⟨hf, ha⟩, ⟨hf', ha'⟩, hB.inst ha⟩
State after:
no goals

State before:
case lamDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
⊢ ClosedN (lam A✝ body✝) (List.length Γ✝) ∧
    ClosedN (lam A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
Tactic:
let ⟨hA, hA', _⟩ := ih1 hΓ
State after:
case lamDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
hA : ClosedN A✝ (List.length Γ✝)
hA' : ClosedN A'✝ (List.length Γ✝)
right✝ : ClosedN (VExpr.sort u✝) (List.length Γ✝)
⊢ ClosedN (lam A✝ body✝) (List.length Γ✝) ∧
    ClosedN (lam A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)

State before:
case lamDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
hA : ClosedN A✝ (List.length Γ✝)
hA' : ClosedN A'✝ (List.length Γ✝)
right✝ : ClosedN (VExpr.sort u✝) (List.length Γ✝)
⊢ ClosedN (lam A✝ body✝) (List.length Γ✝) ∧
    ClosedN (lam A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
Tactic:
let ⟨hb, hb', hB⟩ := ih2 ⟨hΓ, hA⟩
State after:
case lamDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
hA : ClosedN A✝ (List.length Γ✝)
hA' : ClosedN A'✝ (List.length Γ✝)
right✝ : ClosedN (VExpr.sort u✝) (List.length Γ✝)
hb : ClosedN body✝ (List.length (A✝ :: Γ✝))
hb' : ClosedN body'✝ (List.length (A✝ :: Γ✝))
hB : ClosedN B✝ (List.length (A✝ :: Γ✝))
⊢ ClosedN (lam A✝ body✝) (List.length Γ✝) ∧
    ClosedN (lam A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)

State before:
case lamDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
hA : ClosedN A✝ (List.length Γ✝)
hA' : ClosedN A'✝ (List.length Γ✝)
right✝ : ClosedN (VExpr.sort u✝) (List.length Γ✝)
hb : ClosedN body✝ (List.length (A✝ :: Γ✝))
hb' : ClosedN body'✝ (List.length (A✝ :: Γ✝))
hB : ClosedN B✝ (List.length (A✝ :: Γ✝))
⊢ ClosedN (lam A✝ body✝) (List.length Γ✝) ∧
    ClosedN (lam A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
Tactic:
exact ⟨⟨hA, hb⟩, ⟨hA', hb'⟩, hA, hB⟩
State after:
no goals

State before:
case forallEDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN (VExpr.sort v✝) (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
⊢ ClosedN (VExpr.forallE A✝ body✝) (List.length Γ✝) ∧
    ClosedN (VExpr.forallE A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.sort (VLevel.imax u✝ v✝)) (List.length Γ✝)
Tactic:
let ⟨hA, hA', _⟩ := ih1 hΓ
State after:
case forallEDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN (VExpr.sort v✝) (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
hA : ClosedN A✝ (List.length Γ✝)
hA' : ClosedN A'✝ (List.length Γ✝)
right✝ : ClosedN (VExpr.sort u✝) (List.length Γ✝)
⊢ ClosedN (VExpr.forallE A✝ body✝) (List.length Γ✝) ∧
    ClosedN (VExpr.forallE A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.sort (VLevel.imax u✝ v✝)) (List.length Γ✝)

State before:
case forallEDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN (VExpr.sort v✝) (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
hA : ClosedN A✝ (List.length Γ✝)
hA' : ClosedN A'✝ (List.length Γ✝)
right✝ : ClosedN (VExpr.sort u✝) (List.length Γ✝)
⊢ ClosedN (VExpr.forallE A✝ body✝) (List.length Γ✝) ∧
    ClosedN (VExpr.forallE A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.sort (VLevel.imax u✝ v✝)) (List.length Γ✝)
Tactic:
let ⟨hb, hb', _⟩ := ih2 ⟨hΓ, hA⟩
State after:
case forallEDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN (VExpr.sort v✝) (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
hA : ClosedN A✝ (List.length Γ✝)
hA' : ClosedN A'✝ (List.length Γ✝)
right✝¹ : ClosedN (VExpr.sort u✝) (List.length Γ✝)
hb : ClosedN body✝ (List.length (A✝ :: Γ✝))
hb' : ClosedN body'✝ (List.length (A✝ :: Γ✝))
right✝ : ClosedN (VExpr.sort v✝) (List.length (A✝ :: Γ✝))
⊢ ClosedN (VExpr.forallE A✝ body✝) (List.length Γ✝) ∧
    ClosedN (VExpr.forallE A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.sort (VLevel.imax u✝ v✝)) (List.length Γ✝)

State before:
case forallEDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN A'✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN body✝ (List.length (A✝ :: Γ✝)) ∧
      ClosedN body'✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN (VExpr.sort v✝) (List.length (A✝ :: Γ✝))
hΓ : CtxClosed Γ✝
hA : ClosedN A✝ (List.length Γ✝)
hA' : ClosedN A'✝ (List.length Γ✝)
right✝¹ : ClosedN (VExpr.sort u✝) (List.length Γ✝)
hb : ClosedN body✝ (List.length (A✝ :: Γ✝))
hb' : ClosedN body'✝ (List.length (A✝ :: Γ✝))
right✝ : ClosedN (VExpr.sort v✝) (List.length (A✝ :: Γ✝))
⊢ ClosedN (VExpr.forallE A✝ body✝) (List.length Γ✝) ∧
    ClosedN (VExpr.forallE A'✝ body'✝) (List.length Γ✝) ∧ ClosedN (VExpr.sort (VLevel.imax u✝ v✝)) (List.length Γ✝)
Tactic:
exact ⟨⟨hA, hb⟩, ⟨hA', hb'⟩, trivial⟩
State after:
no goals

State before:
case defeqDF
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
ih1 :
  CtxClosed Γ✝ → ClosedN A✝ (List.length Γ✝) ∧ ClosedN B✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort u✝) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN e1✝ (List.length Γ✝) ∧ ClosedN e2✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
⊢ ClosedN e1✝ (List.length Γ✝) ∧ ClosedN e2✝ (List.length Γ✝) ∧ ClosedN B✝ (List.length Γ✝)
Tactic:
exact ⟨(ih2 hΓ).1, (ih2 hΓ).2.1, (ih1 hΓ).2.1⟩
State after:
no goals

State before:
case beta
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
ih2 : CtxClosed Γ✝ → ClosedN e'✝ (List.length Γ✝) ∧ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
⊢ ClosedN (app (lam A✝ e✝) e'✝) (List.length Γ✝) ∧
    ClosedN (inst e✝ e'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ e'✝) (List.length Γ✝)
Tactic:
let ⟨he', _, hA⟩ := ih2 hΓ
State after:
case beta
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
ih2 : CtxClosed Γ✝ → ClosedN e'✝ (List.length Γ✝) ∧ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
he' left✝ : ClosedN e'✝ (List.length Γ✝)
hA : ClosedN A✝ (List.length Γ✝)
⊢ ClosedN (app (lam A✝ e✝) e'✝) (List.length Γ✝) ∧
    ClosedN (inst e✝ e'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ e'✝) (List.length Γ✝)

State before:
case beta
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
ih2 : CtxClosed Γ✝ → ClosedN e'✝ (List.length Γ✝) ∧ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
he' left✝ : ClosedN e'✝ (List.length Γ✝)
hA : ClosedN A✝ (List.length Γ✝)
⊢ ClosedN (app (lam A✝ e✝) e'✝) (List.length Γ✝) ∧
    ClosedN (inst e✝ e'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ e'✝) (List.length Γ✝)
Tactic:
let ⟨he, _, hB⟩ := ih1 ⟨hΓ, hA⟩
State after:
case beta
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
ih2 : CtxClosed Γ✝ → ClosedN e'✝ (List.length Γ✝) ∧ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
he' left✝¹ : ClosedN e'✝ (List.length Γ✝)
hA : ClosedN A✝ (List.length Γ✝)
he left✝ : ClosedN e✝ (List.length (A✝ :: Γ✝))
hB : ClosedN B✝ (List.length (A✝ :: Γ✝))
⊢ ClosedN (app (lam A✝ e✝) e'✝) (List.length Γ✝) ∧
    ClosedN (inst e✝ e'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ e'✝) (List.length Γ✝)

State before:
case beta
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  CtxClosed (A✝ :: Γ✝) →
    ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN e✝ (List.length (A✝ :: Γ✝)) ∧ ClosedN B✝ (List.length (A✝ :: Γ✝))
ih2 : CtxClosed Γ✝ → ClosedN e'✝ (List.length Γ✝) ∧ ClosedN e'✝ (List.length Γ✝) ∧ ClosedN A✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
he' left✝¹ : ClosedN e'✝ (List.length Γ✝)
hA : ClosedN A✝ (List.length Γ✝)
he left✝ : ClosedN e✝ (List.length (A✝ :: Γ✝))
hB : ClosedN B✝ (List.length (A✝ :: Γ✝))
⊢ ClosedN (app (lam A✝ e✝) e'✝) (List.length Γ✝) ∧
    ClosedN (inst e✝ e'✝) (List.length Γ✝) ∧ ClosedN (inst B✝ e'✝) (List.length Γ✝)
Tactic:
exact ⟨⟨⟨hA, he⟩, he'⟩, he.inst he', hB.inst he'⟩
State after:
no goals

State before:
case eta
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  CtxClosed Γ✝ →
    ClosedN e✝ (List.length Γ✝) ∧ ClosedN e✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
hΓ : CtxClosed Γ✝
⊢ ClosedN (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (List.length Γ✝) ∧
    ClosedN e✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
Tactic:
let ⟨he, _, hA, hB⟩ := ih hΓ
State after:
case eta
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  CtxClosed Γ✝ →
    ClosedN e✝ (List.length Γ✝) ∧ ClosedN e✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
hΓ : CtxClosed Γ✝
he left✝ : ClosedN e✝ (List.length Γ✝)
hA : ClosedN A✝ (List.length Γ✝)
hB : ClosedN B✝ (List.length Γ✝ + 1)
⊢ ClosedN (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (List.length Γ✝) ∧
    ClosedN e✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)

State before:
case eta
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  CtxClosed Γ✝ →
    ClosedN e✝ (List.length Γ✝) ∧ ClosedN e✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
hΓ : CtxClosed Γ✝
he left✝ : ClosedN e✝ (List.length Γ✝)
hA : ClosedN A✝ (List.length Γ✝)
hB : ClosedN B✝ (List.length Γ✝ + 1)
⊢ ClosedN (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (List.length Γ✝) ∧
    ClosedN e✝ (List.length Γ✝) ∧ ClosedN (VExpr.forallE A✝ B✝) (List.length Γ✝)
Tactic:
exact ⟨⟨hA, he.liftN, Nat.succ_pos _⟩, he, hA, hB⟩
State after:
no goals

State before:
case proofIrrel
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  CtxClosed Γ✝ →
    ClosedN p✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort VLevel.zero) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN h✝ (List.length Γ✝) ∧ ClosedN h✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
ih3 : CtxClosed Γ✝ → ClosedN h'✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
⊢ ClosedN h✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
Tactic:
let ⟨hh, _, _⟩ := ih2 hΓ
State after:
case proofIrrel
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  CtxClosed Γ✝ →
    ClosedN p✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort VLevel.zero) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN h✝ (List.length Γ✝) ∧ ClosedN h✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
ih3 : CtxClosed Γ✝ → ClosedN h'✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
hh left✝ : ClosedN h✝ (List.length Γ✝)
right✝ : ClosedN p✝ (List.length Γ✝)
⊢ ClosedN h✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)

State before:
case proofIrrel
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  CtxClosed Γ✝ →
    ClosedN p✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort VLevel.zero) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN h✝ (List.length Γ✝) ∧ ClosedN h✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
ih3 : CtxClosed Γ✝ → ClosedN h'✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
hh left✝ : ClosedN h✝ (List.length Γ✝)
right✝ : ClosedN p✝ (List.length Γ✝)
⊢ ClosedN h✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
Tactic:
let ⟨hh', _, hp⟩ := ih3 hΓ
State after:
case proofIrrel
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  CtxClosed Γ✝ →
    ClosedN p✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort VLevel.zero) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN h✝ (List.length Γ✝) ∧ ClosedN h✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
ih3 : CtxClosed Γ✝ → ClosedN h'✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
hh left✝¹ : ClosedN h✝ (List.length Γ✝)
right✝ : ClosedN p✝ (List.length Γ✝)
hh' left✝ : ClosedN h'✝ (List.length Γ✝)
hp : ClosedN p✝ (List.length Γ✝)
⊢ ClosedN h✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)

State before:
case proofIrrel
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  CtxClosed Γ✝ →
    ClosedN p✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝) ∧ ClosedN (VExpr.sort VLevel.zero) (List.length Γ✝)
ih2 : CtxClosed Γ✝ → ClosedN h✝ (List.length Γ✝) ∧ ClosedN h✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
ih3 : CtxClosed Γ✝ → ClosedN h'✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
hΓ : CtxClosed Γ✝
hh left✝¹ : ClosedN h✝ (List.length Γ✝)
right✝ : ClosedN p✝ (List.length Γ✝)
hh' left✝ : ClosedN h'✝ (List.length Γ✝)
hp : ClosedN p✝ (List.length Γ✝)
⊢ ClosedN h✝ (List.length Γ✝) ∧ ClosedN h'✝ (List.length Γ✝) ∧ ClosedN p✝ (List.length Γ✝)
Tactic:
exact ⟨hh, hh', hp⟩
State after:
no goals

State before:
case extra
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
a✝¹ : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝ : List.length ls✝ = df✝.uvars
hΓ : CtxClosed Γ✝
⊢ ClosedN (instL ls✝ df✝.lhs) (List.length Γ✝) ∧
    ClosedN (instL ls✝ df✝.rhs) (List.length Γ✝) ∧ ClosedN (instL ls✝ df✝.type) (List.length Γ✝)
Tactic:
let ⟨⟨hl, _⟩, ⟨hr, hA⟩⟩ := henv.2 h1
State after:
case extra
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
a✝¹ : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝ : List.length ls✝ = df✝.uvars
hΓ : CtxClosed Γ✝
hl : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hr : ClosedN df✝.rhs
hA : ClosedN df✝.type
⊢ ClosedN (instL ls✝ df✝.lhs) (List.length Γ✝) ∧
    ClosedN (instL ls✝ df✝.rhs) (List.length Γ✝) ∧ ClosedN (instL ls✝ df✝.type) (List.length Γ✝)

State before:
case extra
env : VEnv
henv : OnTypes env fun x e A => ClosedN e ∧ ClosedN A
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
a✝¹ : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝ : List.length ls✝ = df✝.uvars
hΓ : CtxClosed Γ✝
hl : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hr : ClosedN df✝.rhs
hA : ClosedN df✝.type
⊢ ClosedN (instL ls✝ df✝.lhs) (List.length Γ✝) ∧
    ClosedN (instL ls✝ df✝.rhs) (List.length Γ✝) ∧ ClosedN (instL ls✝ df✝.type) (List.length Γ✝)
Tactic:
exact ⟨
  hl.instL.mono (Nat.zero_le _),
  hr.instL.mono (Nat.zero_le _),
  hA.instL.mono (Nat.zero_le _)⟩
State after:
no goals