Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv' (Lean4Lean/Theory/Typing/Strong.lean)

State before:
case symm
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : e'✝ = forallE A B ∨ e✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih hΓ eq.symm
State after:
no goals

State before:
case proofIrrel
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : h✝ = forallE A B ∨ h'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
obtain eq | eq := eq
State after:
case proofIrrel.inl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : h✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)

case proofIrrel.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : h'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)

State before:
case proofIrrel.inl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : h✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih1 hΓ (.inl eq)
State after:
no goals

State before:
case proofIrrel.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : h'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih2 hΓ (.inr eq)
State after:
no goals

State before:
case forallEDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝² : VLevel.WF U u✝
a✝¹ : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A'✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A'✝ :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : forallE A✝ body✝ = forallE A B ∨ forallE A'✝ body'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
obtain ⟨⟨⟩⟩ | ⟨⟨⟩⟩ := eq
State after:
case forallEDF.inl.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝² : VLevel.WF U u✝
a✝¹ : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A'✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A'✝ :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
⊢ (∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)) ∧ ∃ v, IsDefEqStrong env U (A✝ :: Γ✝) body✝ body✝ (sort v)

case forallEDF.inr.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝² : VLevel.WF U u✝
a✝¹ : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A'✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A'✝ :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
⊢ (∃ u, IsDefEqStrong env U Γ✝ A'✝ A'✝ (sort u)) ∧ ∃ v, IsDefEqStrong env U (A'✝ :: Γ✝) body'✝ body'✝ (sort v)

State before:
case forallEDF.inl.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝² : VLevel.WF U u✝
a✝¹ : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A'✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A'✝ :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
⊢ (∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)) ∧ ∃ v, IsDefEqStrong env U (A✝ :: Γ✝) body✝ body✝ (sort v)
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 (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝² : VLevel.WF U u✝
a✝¹ : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A'✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A'✝ :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
⊢ (∃ u, IsDefEqStrong env U Γ✝ A'✝ A'✝ (sort u)) ∧ ∃ v, IsDefEqStrong env U (A'✝ :: Γ✝) body'✝ body'✝ (sort v)
Tactic:
exact ⟨⟨_, h1.hasType.2⟩, _, h1.defeqDF_l henv hΓ h2.hasType.2⟩
State after:
no goals

State before:
case defeqDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝² : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e1✝ = forallE A B ∨ e2✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : e1✝ = forallE A B ∨ e2✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih2 hΓ eq
State after:
no goals

State before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h3 : IsDefEqStrong env U (A✝ :: Γ✝) e e B✝
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e e'✝) (inst e e'✝) (inst B✝ e'✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      e = forallE A B ∨ e = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst e e'✝ = forallE A B ∨ inst e e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : app (lam A✝ e) e'✝ = forallE A B ∨ inst e e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
State after:
case beta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h3 : IsDefEqStrong env U (A✝ :: Γ✝) e e B✝
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e e'✝) (inst e e'✝) (inst B✝ e'✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      e = forallE A B ∨ e = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst e e'✝ = forallE A B ∨ inst e e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : inst e e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)

State before:
case beta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h3 : IsDefEqStrong env U (A✝ :: Γ✝) e e B✝
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e e'✝) (inst e e'✝) (inst B✝ e'✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      e = forallE A B ∨ e = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst e e'✝ = forallE A B ∨ inst e e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : inst e e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
cases e with
| bvar i =>
  cases i with simp [inst] at eq
  | zero => exact ih4 hΓ (.inl eq)
| forallE A B =>
  cases eq
  let ⟨⟨_, A1⟩, _, A2⟩ := ih3 ⟨hΓ, _, h1⟩ (.inl rfl)
  refine ⟨⟨_, h4.instN henv hΓ .zero A1 hΓ⟩, _, h4.instN henv hΓ (.succ .zero) A2 ?_⟩
  exact ⟨hΓ, _, h4.instN henv hΓ .zero A1 hΓ⟩
| _ => cases eq
State after:
no goals

State before:
case beta.inr.bvar
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
i : Nat
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (VExpr.bvar i) (VExpr.bvar i) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (VExpr.bvar i) e'✝) (inst (VExpr.bvar i) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      VExpr.bvar i = forallE A B ∨ VExpr.bvar i = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst (VExpr.bvar i) e'✝ = forallE A B ∨ inst (VExpr.bvar i) e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
eq : inst (VExpr.bvar i) e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
cases i with simp [inst] at eq
| zero => exact ih4 hΓ (.inl eq)
State after:
no goals

State before:
case beta.inr.bvar.zero
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (VExpr.bvar Nat.zero) (VExpr.bvar Nat.zero) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (VExpr.bvar Nat.zero) e'✝) (inst (VExpr.bvar Nat.zero) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      VExpr.bvar Nat.zero = forallE A B ∨ VExpr.bvar Nat.zero = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst (VExpr.bvar Nat.zero) e'✝ = forallE A B ∨ inst (VExpr.bvar Nat.zero) e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
eq : e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih4 hΓ (.inl eq)
State after:
no goals

State before:
case beta.inr.forallE
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝¹ : VExpr
u✝ : VLevel
B✝¹ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝¹ A✝¹ (sort u✝)
h2 : IsDefEqStrong env U (A✝¹ :: Γ✝) B✝¹ B✝¹ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝¹
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝¹ e'✝) (inst B✝¹ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝¹ = forallE A B ∨ A✝¹ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝¹ :: Γ✝) →
      B✝¹ = forallE A B ∨ B✝¹ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝¹ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝¹ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝¹ e'✝ = forallE A B ∨ inst B✝¹ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A✝ B✝ : VExpr
hΓ : CtxStrong env U Γ✝
A B : VExpr
h3 : IsDefEqStrong env U (A✝¹ :: Γ✝) (forallE A B) (forallE A B) B✝¹
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝¹ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝¹ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝¹ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝¹ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
eq : inst (forallE A B) e'✝ = forallE A✝ B✝
⊢ (∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)) ∧ ∃ v, IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v)
Tactic:
cases eq
State after:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
A B : VExpr
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (forallE A B) (forallE A B) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
⊢ (∃ u, IsDefEqStrong env U Γ✝ (inst A e'✝) (inst A e'✝) (sort u)) ∧
    ∃ v, IsDefEqStrong env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1)) (inst B e'✝ (0 + 1)) (sort v)

State before:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
A B : VExpr
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (forallE A B) (forallE A B) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
⊢ (∃ u, IsDefEqStrong env U Γ✝ (inst A e'✝) (inst A e'✝) (sort u)) ∧
    ∃ v, IsDefEqStrong env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1)) (inst B e'✝ (0 + 1)) (sort v)
Tactic:
let ⟨⟨_, A1⟩, _, A2⟩ := ih3 ⟨hΓ, _, h1⟩ (.inl rfl)
State after:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
A B : VExpr
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (forallE A B) (forallE A B) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
w✝¹ : VLevel
A1 : IsDefEqStrong env U (A✝ :: Γ✝) A A (sort w✝¹)
w✝ : VLevel
A2 : IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort w✝)
⊢ (∃ u, IsDefEqStrong env U Γ✝ (inst A e'✝) (inst A e'✝) (sort u)) ∧
    ∃ v, IsDefEqStrong env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1)) (inst B e'✝ (0 + 1)) (sort v)

State before:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
A B : VExpr
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (forallE A B) (forallE A B) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
w✝¹ : VLevel
A1 : IsDefEqStrong env U (A✝ :: Γ✝) A A (sort w✝¹)
w✝ : VLevel
A2 : IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort w✝)
⊢ (∃ u, IsDefEqStrong env U Γ✝ (inst A e'✝) (inst A e'✝) (sort u)) ∧
    ∃ v, IsDefEqStrong env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1)) (inst B e'✝ (0 + 1)) (sort v)
Tactic:
refine ⟨⟨_, h4.instN henv hΓ .zero A1 hΓ⟩, _, h4.instN henv hΓ (.succ .zero) A2 ?_⟩
State after:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
A B : VExpr
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (forallE A B) (forallE A B) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
w✝¹ : VLevel
A1 : IsDefEqStrong env U (A✝ :: Γ✝) A A (sort w✝¹)
w✝ : VLevel
A2 : IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort w✝)
⊢ CtxStrong env U (inst A e'✝ :: Γ✝)

State before:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
hΓ : CtxStrong env U Γ✝
A B : VExpr
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (forallE A B) (forallE A B) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
w✝¹ : VLevel
A1 : IsDefEqStrong env U (A✝ :: Γ✝) A A (sort w✝¹)
w✝ : VLevel
A2 : IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort w✝)
⊢ CtxStrong env U (inst A e'✝ :: Γ✝)
Tactic:
exact ⟨hΓ, _, h4.instN henv hΓ .zero A1 hΓ⟩
State after:
no goals

State before:
case beta.inr.lam
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
binderType✝ body✝ : VExpr
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (lam binderType✝ body✝) (lam binderType✝ body✝) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (lam binderType✝ body✝) e'✝) (inst (lam binderType✝ body✝) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      lam binderType✝ body✝ = forallE A B ∨ lam binderType✝ body✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      inst (lam binderType✝ body✝) e'✝ = forallE A B ∨ inst (lam binderType✝ body✝) e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
eq : inst (lam binderType✝ body✝) e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
cases eq
State after:
no goals

State before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (lift A✝ :: A✝ :: Γ✝) →
      liftN 1 B✝ 1 = forallE A B ∨ liftN 1 B✝ 1 = forallE A B →
        (∃ u, IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) A A (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A :: lift A✝ :: A✝ :: Γ✝) B B (sort v)
ih :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e✝ = forallE A B ∨ e✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      lift e✝ = forallE A B ∨ lift e✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : lam A✝ (app (lift e✝) (VExpr.bvar 0)) = forallE A B ∨ e✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
State after:
case eta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (lift A✝ :: A✝ :: Γ✝) →
      liftN 1 B✝ 1 = forallE A B ∨ liftN 1 B✝ 1 = forallE A B →
        (∃ u, IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) A A (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A :: lift A✝ :: A✝ :: Γ✝) B B (sort v)
ih :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e✝ = forallE A B ∨ e✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      lift e✝ = forallE A B ∨ lift e✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : e✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)

State before:
case eta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (lift A✝ :: A✝ :: Γ✝) →
      liftN 1 B✝ 1 = forallE A B ∨ liftN 1 B✝ 1 = forallE A B →
        (∃ u, IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) A A (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A :: lift A✝ :: A✝ :: Γ✝) B B (sort v)
ih :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e✝ = forallE A B ∨ e✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      lift e✝ = forallE A B ∨ lift e✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : e✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih hΓ (.inl eq)
State after:
no goals

State before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ
eq : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
Tactic:
suffices ∀ e, VExpr.instL ls e = VExpr.forallE A B →
    EnvStrong env df.uvars e df.type →
    (∃ u, IsDefEqStrong env U Γ A A (.sort u)) ∧
    (∃ u, IsDefEqStrong env U (A :: Γ) B B (.sort u)) by
  have ⟨A1, A2⟩ := envIH.2 h1
  cases eq <;> exact this _ ‹_› ‹_›
State after:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ
eq : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
⊢ ∀ (e : VExpr),
    VExpr.instL ls e = forallE A B →
      EnvStrong env df.uvars e df.type →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)

State before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ
eq : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
⊢ ∀ (e : VExpr),
    VExpr.instL ls e = forallE A B →
      EnvStrong env df.uvars e df.type →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)
Tactic:
intro e eq IH
State after:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ
eq✝ : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
e : VExpr
eq : VExpr.instL ls e = forallE A B
IH : EnvStrong env df.uvars e df.type
⊢ (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)

State before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ
eq✝ : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
e : VExpr
eq : VExpr.instL ls e = forallE A B
IH : EnvStrong env df.uvars e df.type
⊢ (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)
Tactic:
cases e <;> cases eq
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
binderType✝ body✝ : VExpr
IH : EnvStrong env df.uvars (forallE binderType✝ body✝) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝)
⊢ (∃ u, IsDefEqStrong env U Γ (VExpr.instL ls binderType✝) (VExpr.instL ls binderType✝) (sort u)) ∧
    ∃ u, IsDefEqStrong env U (VExpr.instL ls binderType✝ :: Γ) (VExpr.instL ls body✝) (VExpr.instL ls body✝) (sort u)

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
binderType✝ body✝ : VExpr
IH : EnvStrong env df.uvars (forallE binderType✝ body✝) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝)
⊢ (∃ u, IsDefEqStrong env U Γ (VExpr.instL ls binderType✝) (VExpr.instL ls binderType✝) (sort u)) ∧
    ∃ u, IsDefEqStrong env U (VExpr.instL ls binderType✝ :: Γ) (VExpr.instL ls body✝) (VExpr.instL ls body✝) (sort u)
Tactic:
rename_i A B
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
⊢ (∃ u, IsDefEqStrong env U Γ (VExpr.instL ls A) (VExpr.instL ls A) (sort u)) ∧
    ∃ u, IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort u)

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
⊢ (∃ u, IsDefEqStrong env U Γ (VExpr.instL ls A) (VExpr.instL ls A) (sort u)) ∧
    ∃ u, IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort u)
Tactic:
let ⟨⟨_, A1⟩, v, A2⟩ := IH.2.2 _ _ rfl
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
⊢ (∃ u, IsDefEqStrong env U Γ (VExpr.instL ls A) (VExpr.instL ls A) (sort u)) ∧
    ∃ u, IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort u)

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
⊢ (∃ u, IsDefEqStrong env U Γ (VExpr.instL ls A) (VExpr.instL ls A) (sort u)) ∧
    ∃ u, IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort u)
Tactic:
refine ⟨⟨_, (A1.instL h2).weak0 henv⟩, v.inst ls, ?_⟩
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (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 (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong 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 B) (0 + 1))
    (liftN (List.length Γ) (VExpr.instL ls (sort v)) (0 + 1))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong 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 B) (0 + 1))
    (liftN (List.length Γ) (VExpr.instL ls (sort v)) (0 + 1))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))
Tactic:
have C1 := (A1.instL h2).defeq.closedN henv ⟨⟩
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong 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 B) (0 + 1))
    (liftN (List.length Γ) (VExpr.instL ls (sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong 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 B) (0 + 1))
    (liftN (List.length Γ) (VExpr.instL ls (sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))
Tactic:
have C2 := (A2.instL h2).defeq.closedN henv ⟨⟨⟩, C1⟩
State after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong 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 B) (0 + 1))
    (liftN (List.length Γ) (VExpr.instL ls (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]))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong 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 B) (0 + 1))
    (liftN (List.length Γ) (VExpr.instL ls (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]))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (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 (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) [])) (VExpr.instL ls B) (VExpr.instL ls B)
    (liftN (List.length Γ) (VExpr.instL ls (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]))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))

State before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) [])) (VExpr.instL ls B) (VExpr.instL ls B)
    (liftN (List.length Γ) (VExpr.instL ls (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]))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))
Tactic:
simpa [liftN]
State after:
no goals

State before:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ
eq : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = forallE A B →
      EnvStrong env df.uvars e df.type →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)
⊢ (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
Tactic:
have ⟨A1, A2⟩ := envIH.2 h1
State after:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ
eq : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = forallE A B →
      EnvStrong env df.uvars e df.type →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)
A1 : EnvStrong env df.uvars df.lhs df.type
A2 : EnvStrong env df.uvars df.rhs df.type
⊢ (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)

State before:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ
eq : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = forallE A B →
      EnvStrong env df.uvars e df.type →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)
A1 : EnvStrong env df.uvars df.lhs df.type
A2 : EnvStrong env df.uvars df.rhs df.type
⊢ (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
Tactic:
cases eq <;> exact this _ ‹_› ‹_›
State after:
no goals

State before:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝⁶ : List.length ls = df.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls df.type) (VExpr.instL ls df.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a✝¹ : IsDefEqStrong env U Γ (VExpr.instL ls df.lhs) (VExpr.instL ls df.lhs) (VExpr.instL ls df.type)
a✝ : IsDefEqStrong env U Γ (VExpr.instL ls df.rhs) (VExpr.instL ls df.rhs) (VExpr.instL ls df.type)
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong 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 B) (0 + 1))
    (liftN (List.length Γ) (VExpr.instL ls (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 (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A'✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A'✝ :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A'✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A'✝ :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : lam A✝ body✝ = forallE A B ∨ lam A'✝ body'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
nomatch eq
State after:
no goals