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

State before:
case symm
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : ∀ {A B : VExpr}, e✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : e'✝ = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih eq.symm
State after:
no goals

State before:
case proofIrrel
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
obtain eq | eq := eq
State after:
case proofIrrel.inl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B

case proofIrrel.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B

State before:
case proofIrrel.inl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih1 (.inl eq)
State after:
no goals

State before:
case proofIrrel.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih2 (.inr eq)
State after:
no goals

State before:
case forallEDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a_ih✝¹ :
  ∀ {A B : VExpr}, A✝ = VExpr.forallE A B ∨ A'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
a_ih✝ :
  ∀ {A B : VExpr},
    body✝ = VExpr.forallE A B ∨ body'✝ = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
A B : VExpr
eq : VExpr.forallE A✝ body✝ = VExpr.forallE A B ∨ VExpr.forallE A'✝ body'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
obtain ⟨⟨⟩⟩ | ⟨⟨⟩⟩ := eq
State after:
case forallEDF.inl.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a_ih✝¹ :
  ∀ {A B : VExpr}, A✝ = VExpr.forallE A B ∨ A'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
a_ih✝ :
  ∀ {A B : VExpr},
    body✝ = VExpr.forallE A B ∨ body'✝ = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
⊢ IsType env U Γ✝ A✝ ∧ IsType env U (A✝ :: Γ✝) body✝

case forallEDF.inr.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a_ih✝¹ :
  ∀ {A B : VExpr}, A✝ = VExpr.forallE A B ∨ A'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
a_ih✝ :
  ∀ {A B : VExpr},
    body✝ = VExpr.forallE A B ∨ body'✝ = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
⊢ IsType env U Γ✝ A'✝ ∧ IsType env U (A'✝ :: Γ✝) body'✝

State before:
case forallEDF.inl.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a_ih✝¹ :
  ∀ {A B : VExpr}, A✝ = VExpr.forallE A B ∨ A'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
a_ih✝ :
  ∀ {A B : VExpr},
    body✝ = VExpr.forallE A B ∨ body'✝ = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
⊢ IsType env U Γ✝ A✝ ∧ IsType env U (A✝ :: Γ✝) body✝
Tactic:
exact ⟨⟨_, h1.hasType.1⟩, _, h2.hasType.1⟩
State after:
no goals

State before:
case forallEDF.inr.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a_ih✝¹ :
  ∀ {A B : VExpr}, A✝ = VExpr.forallE A B ∨ A'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
a_ih✝ :
  ∀ {A B : VExpr},
    body✝ = VExpr.forallE A B ∨ body'✝ = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
⊢ IsType env U Γ✝ A'✝ ∧ IsType env U (A'✝ :: Γ✝) body'✝
Tactic:
exact ⟨⟨_, h1.hasType.2⟩, _, h2.hasType.2.defeq_l henv h1⟩
State after:
no goals

State before:
case defeqDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : 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✝
a_ih✝ : ∀ {A B : VExpr}, A✝ = VExpr.forallE A B ∨ B✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, e1✝ = VExpr.forallE A B ∨ e2✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : e1✝ = VExpr.forallE A B ∨ e2✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih2 eq
State after:
no goals

State before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
e B✝ e'✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) e e B✝
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  ∀ {A B : VExpr},
    e = VExpr.forallE A B ∨ e = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : app (lam A✝ e) e'✝ = VExpr.forallE A B ∨ inst e e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
State after:
case beta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
e B✝ e'✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) e e B✝
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  ∀ {A B : VExpr},
    e = VExpr.forallE A B ∨ e = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : inst e e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B

State before:
case beta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
e B✝ e'✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) e e B✝
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  ∀ {A B : VExpr},
    e = VExpr.forallE A B ∨ e = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : inst e e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
cases e with
| bvar i =>
  cases i with simp [inst] at eq
  | zero => exact ih2 (.inl eq)
| forallE A B =>
  cases eq
  let ⟨A1, A2⟩ := ih1 (.inl rfl)
  exact ⟨A1.instN henv .zero h2, A2.instN henv (.succ .zero) h2⟩
| _ => cases eq
State after:
no goals

State before:
case beta.inr.bvar
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
i : Nat
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.bvar i) (VExpr.bvar i) B✝
ih1 :
  ∀ {A B : VExpr},
    VExpr.bvar i = VExpr.forallE A B ∨ VExpr.bvar i = VExpr.forallE A B →
      IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
eq : inst (VExpr.bvar i) e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
cases i with simp [inst] at eq
| zero => exact ih2 (.inl eq)
State after:
no goals

State before:
case beta.inr.bvar.zero
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.bvar Nat.zero) (VExpr.bvar Nat.zero) B✝
ih1 :
  ∀ {A B : VExpr},
    VExpr.bvar Nat.zero = VExpr.forallE A B ∨ VExpr.bvar Nat.zero = VExpr.forallE A B →
      IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
eq : e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih2 (.inl eq)
State after:
no goals

State before:
case beta.inr.forallE
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝¹ : VExpr
Γ✝ : List VExpr
B✝¹ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝¹
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A✝ B✝ A B : VExpr
h1 : IsDefEq env U (A✝¹ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝¹
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝¹ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝¹ :: Γ✝) B_1
eq : inst (VExpr.forallE A B) e'✝ = VExpr.forallE A✝ B✝
⊢ IsType env U Γ✝ A✝ ∧ IsType env U (A✝ :: Γ✝) B✝
Tactic:
cases eq
State after:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝ :: Γ✝) B_1
⊢ IsType env U Γ✝ (inst A e'✝) ∧ IsType env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1))

State before:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝ :: Γ✝) B_1
⊢ IsType env U Γ✝ (inst A e'✝) ∧ IsType env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1))
Tactic:
let ⟨A1, A2⟩ := ih1 (.inl rfl)
State after:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝ :: Γ✝) B_1
A1 : IsType env U (A✝ :: Γ✝) A
A2 : IsType env U (A :: A✝ :: Γ✝) B
⊢ IsType env U Γ✝ (inst A e'✝) ∧ IsType env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1))

State before:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝ :: Γ✝) B_1
A1 : IsType env U (A✝ :: Γ✝) A
A2 : IsType env U (A :: A✝ :: Γ✝) B
⊢ IsType env U Γ✝ (inst A e'✝) ∧ IsType env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1))
Tactic:
exact ⟨A1.instN henv .zero h2, A2.instN henv (.succ .zero) h2⟩
State after:
no goals

State before:
case beta.inr.lam
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B binderType✝ body✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (lam binderType✝ body✝) (lam binderType✝ body✝) B✝
ih1 :
  ∀ {A B : VExpr},
    lam binderType✝ body✝ = VExpr.forallE A B ∨ lam binderType✝ body✝ = VExpr.forallE A B →
      IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
eq : inst (lam binderType✝ body✝) e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
cases eq
State after:
no goals

State before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : ∀ {A B : VExpr}, e✝ = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : lam A✝ (app (lift e✝) (VExpr.bvar 0)) = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
State after:
case eta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : ∀ {A B : VExpr}, e✝ = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : e✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B

State before:
case eta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : ∀ {A B : VExpr}, e✝ = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : e✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih (.inl eq)
State after:
no goals

State before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
suffices ∀ e, VExpr.instL ls e = VExpr.forallE A B →
    (∀ A B, e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B) →
    IsType env U Γ A ∧ IsType env U (A :: Γ) B by
  have ⟨A1, A2⟩ := envIH.2 h1
  cases eq <;> exact this _ ‹_› ‹_›
State after:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
⊢ ∀ (e : VExpr),
    VExpr.instL ls e = VExpr.forallE A B →
      (∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B) →
        IsType env U Γ A ∧ IsType env U (A :: Γ) B

State before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
⊢ ∀ (e : VExpr),
    VExpr.instL ls e = VExpr.forallE A B →
      (∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B) →
        IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
intro e eq IH
State after:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq✝ : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
e : VExpr
eq : VExpr.instL ls e = VExpr.forallE A B
IH : ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B

State before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq✝ : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
e : VExpr
eq : VExpr.instL ls e = VExpr.forallE A B
IH : ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
cases e <;> cases eq
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
binderType✝ body✝ : VExpr
IH :
  ∀ (A B : VExpr),
    VExpr.forallE binderType✝ body✝ = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝)
⊢ IsType env U Γ (VExpr.instL ls binderType✝) ∧ IsType env U (VExpr.instL ls binderType✝ :: Γ) (VExpr.instL ls body✝)

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
binderType✝ body✝ : VExpr
IH :
  ∀ (A B : VExpr),
    VExpr.forallE binderType✝ body✝ = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝)
⊢ IsType env U Γ (VExpr.instL ls binderType✝) ∧ IsType env U (VExpr.instL ls binderType✝ :: Γ) (VExpr.instL ls body✝)
Tactic:
rename_i A B
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
⊢ IsType env U Γ (VExpr.instL ls A) ∧ IsType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B)

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
⊢ IsType env U Γ (VExpr.instL ls A) ∧ IsType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B)
Tactic:
let ⟨⟨_, A1⟩, v, A2⟩ := IH _ _ rfl
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
⊢ IsType env U Γ (VExpr.instL ls A) ∧ IsType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B)

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
⊢ IsType env U Γ (VExpr.instL ls A) ∧ IsType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B)
Tactic:
refine ⟨⟨_, (A1.instL h2).weak0 henv⟩, v.inst ls, ?_⟩
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
have := (A2.instL h2).weakN henv (.succ (.zero Γ))
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
have C1 := (A1.instL h2).closedN henv ⟨⟩
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
have C2 := (A2.instL h2).closedN henv ⟨⟨⟩, C1⟩
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
C2 : ClosedN (VExpr.instL ls B) (List.length (List.map (VExpr.instL ls) [A]))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
C2 : ClosedN (VExpr.instL ls B) (List.length (List.map (VExpr.instL ls) [A]))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
rw [C1.liftN_eq (Nat.zero_le _), C2.liftN_eq (by exact Nat.le_refl _)] at this
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) [])) (VExpr.instL ls B)
    (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
C2 : ClosedN (VExpr.instL ls B) (List.length (List.map (VExpr.instL ls) [A]))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) [])) (VExpr.instL ls B)
    (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
C2 : ClosedN (VExpr.instL ls B) (List.length (List.map (VExpr.instL ls) [A]))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
simpa [liftN]
State after:
no goals

State before:
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = VExpr.forallE A B →
      (∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B) →
        IsType env U Γ A ∧ IsType env U (A :: Γ) B
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
have ⟨A1, A2⟩ := envIH.2 h1
State after:
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = VExpr.forallE A B →
      (∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B) →
        IsType env U Γ A ∧ IsType env U (A :: Γ) B
A1 :
  (fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B) df.uvars df.lhs df.type
A2 :
  (fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B) df.uvars df.rhs df.type
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B

State before:
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = VExpr.forallE A B →
      (∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B) →
        IsType env U Γ A ∧ IsType env U (A :: Γ) B
A1 :
  (fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B) df.uvars df.lhs df.type
A2 :
  (fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B) df.uvars df.rhs df.type
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
cases eq <;> exact this _ ‹_› ‹_›
State after:
no goals

State before:
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
C2 : ClosedN (VExpr.instL ls B) (List.length (List.map (VExpr.instL ls) [A]))
⊢ List.length (List.map (VExpr.instL ls) [A]) ≤ 0 + 1
Tactic:
exact Nat.le_refl _
State after:
no goals

State before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : 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✝
a_ih✝¹ :
  ∀ {A B : VExpr}, A✝ = VExpr.forallE A B ∨ A'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
a_ih✝ :
  ∀ {A B : VExpr},
    body✝ = VExpr.forallE A B ∨ body'✝ = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
A B : VExpr
eq : lam A✝ body✝ = VExpr.forallE A B ∨ lam A'✝ body'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
nomatch eq
State after:
no goals