Theorem: Lean4Lean.VEnv.IsDefEq.inductionU1 (Lean4Lean/Theory/Typing/StratifiedUntyped.lean)

State before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H : IsDefEq env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2
Tactic:
have H' := H.strong henv hΓ
State after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H : IsDefEq env U Γ e1 e2 A
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2

State before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H : IsDefEq env U Γ e1 e2 A
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2
Tactic:
clear hΓ H
State after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2

State before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2
Tactic:
induction H' with
| bvar h => exact ⟨.bvar h, .bvar h, .refl⟩
| symm _ ih => exact ⟨ih.2.1, ih.1, .symm ih.2.2⟩
| trans _ _ ih1 ih2 => exact ⟨ih1.1, ih2.2.1, .trans ih1.2.2 ih2.2.2⟩
| @constDF _ _ ls₁ ls₂ _ _ h1 h2 h3 h4 h5 =>
  exact ⟨.const h1 h2 h4, .defeq sorry <| .const h1 h3 (h5.length_eq.symm.trans h4), .constDF h5⟩
| @sortDF l l' _ h1 h2 h3 =>
  refine ⟨.sort h1, ?_, .sortDF h3⟩
  exact .defeq (hdf (.sort (l := l'.succ) h2) (.sort (l := l.succ) h1)
    (.sortDF <| VLevel.succ_congr h3.symm)) (.sort h2)
| appDF _ _ _ _ _ _ _ _ _ ihf iha ihBa =>
  let ⟨hf, hf', ff⟩ := ihf; let ⟨ha, ha', aa⟩ := iha
  exact ⟨.app hf ha, .defeq (hdf ihBa.2.1 ihBa.1 (.symm ihBa.2.2)) (.app hf' ha'), .appDF ff aa⟩
| lamDF _ _ _ _ _ _ _ ihA ihB ihB' ihb ihb' =>
  refine ⟨.lam ihA.1 ihb.1, .defeq ?_ <| .lam ihA.2.1 ihb'.2.1, .lamDF ihA.2.2 ihb.2.2⟩
  exact hdf (.forallE ihA.2.1 ihB'.1) (.forallE ihA.1 ihB.1) <|
    .symm <| .forallEDF ihA.2.2 ihB.2.2
| forallEDF _ _ _ _ _ ih1 ih2 ih3 =>
  exact ⟨.forallE ih1.1 ih2.1, .forallE ih1.2.1 ih3.2.1, .forallEDF ih1.2.2 ih2.2.2⟩
| defeqDF _ _ _ ih1 ih2 =>
  have h := hdf ih1.1 ih1.2.1 ih1.2.2; exact ⟨.defeq h ih2.1, .defeq h ih2.2.1, ih2.2.2⟩
| beta _ _ _ _ _ _ _ _ ihA _ ihe ihe' _ ihee =>
  exact ⟨.app (.lam ihA.1 ihe.1) ihe'.1, ihee.1, .beta (hty ihe.1) (hty ihe'.1)⟩
| eta _ _ _ _ _ _ _ ihA _ _ ihe ihe' =>
  have := HasTypeU1.app ihe'.1 (.bvar .zero)
  rw [instN_bvar0] at this
  exact ⟨.lam ihA.1 this, ihe.1, .eta⟩
| proofIrrel _ _ _ ih1 ih2 ih3 =>
  exact ⟨ih2.1, ih3.1, .proofIrrel (hty ih1.1) (hty ih2.1) (hty ih3.1)⟩
| extra h1 h2 h3 _ _ _ _ _ _ _ _ _ ihl' ihr' =>
  exact ⟨ihl'.1, ihr'.1, .extra h1 h2 h3⟩
State after:
no goals

State before:
case bvar
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
u✝ : VLevel
h : Lookup Γ✝ i✝ A✝
a✝¹ : VLevel.WF U u✝
a✝ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a_ih✝ :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
⊢ HasTypeU1 env U defEq Γ✝ (VExpr.bvar i✝) A✝ ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.bvar i✝) A✝ ∧ IsDefEqU1 env U hasType Γ✝ (VExpr.bvar i✝) (VExpr.bvar i✝)
Tactic:
exact ⟨.bvar h, .bvar h, .refl⟩
State after:
no goals

State before:
case symm
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih : HasTypeU1 env U defEq Γ✝ e✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e✝ e'✝
⊢ HasTypeU1 env U defEq Γ✝ e'✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e'✝ e✝
Tactic:
exact ⟨ih.2.1, ih.1, .symm ih.2.2⟩
State after:
no goals

State before:
case trans
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEqStrong env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEqStrong env U Γ✝ e₂✝ e₃✝ A✝
ih1 : HasTypeU1 env U defEq Γ✝ e₁✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e₂✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e₁✝ e₂✝
ih2 : HasTypeU1 env U defEq Γ✝ e₂✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e₃✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e₂✝ e₃✝
⊢ HasTypeU1 env U defEq Γ✝ e₁✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e₃✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e₁✝ e₃✝
Tactic:
exact ⟨ih1.1, ih2.2.1, .trans ih1.2.2 ih2.2.2⟩
State after:
no goals

State before:
case constDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
c✝ : Name
ci✝ : VConstant
ls₁ ls₂ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls₁ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls₂ → VLevel.WF U l
h4 : List.length ls₁ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls₁ ls₂
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type) (VExpr.sort u✝)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls₂ ci✝.type) (VExpr.instL ls₂ ci✝.type) (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type) (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls₂ ci✝.type) (VExpr.instL ls₂ ci✝.type) (VExpr.sort u✝)
a_ih✝³ :
  HasTypeU1 env U defEq [] (VExpr.instL ls₁ ci✝.type) (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq [] (VExpr.instL ls₁ ci✝.type) (VExpr.sort u✝) ∧
      IsDefEqU1 env U hasType [] (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type)
a_ih✝² :
  HasTypeU1 env U defEq [] (VExpr.instL ls₂ ci✝.type) (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq [] (VExpr.instL ls₂ ci✝.type) (VExpr.sort u✝) ∧
      IsDefEqU1 env U hasType [] (VExpr.instL ls₂ ci✝.type) (VExpr.instL ls₂ ci✝.type)
a_ih✝¹ :
  HasTypeU1 env U defEq Γ✝ (VExpr.instL ls₁ ci✝.type) (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.instL ls₁ ci✝.type) (VExpr.sort u✝) ∧
      IsDefEqU1 env U hasType Γ✝ (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type)
a_ih✝ :
  HasTypeU1 env U defEq Γ✝ (VExpr.instL ls₂ ci✝.type) (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.instL ls₂ ci✝.type) (VExpr.sort u✝) ∧
      IsDefEqU1 env U hasType Γ✝ (VExpr.instL ls₂ ci✝.type) (VExpr.instL ls₂ ci✝.type)
⊢ HasTypeU1 env U defEq Γ✝ (VExpr.const c✝ ls₁) (VExpr.instL ls₁ ci✝.type) ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type) ∧
      IsDefEqU1 env U hasType Γ✝ (VExpr.const c✝ ls₁) (VExpr.const c✝ ls₂)
Tactic:
exact ⟨.const h1 h2 h4, .defeq sorry <| .const h1 h3 (h5.length_eq.symm.trans h4), .constDF h5⟩
State after:
no goals

State before:
case sortDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
l l' : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l
h2 : VLevel.WF U l'
h3 : l ≈ l'
⊢ HasTypeU1 env U defEq Γ✝ (VExpr.sort l) (VExpr.sort (VLevel.succ l)) ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.sort l') (VExpr.sort (VLevel.succ l)) ∧
      IsDefEqU1 env U hasType Γ✝ (VExpr.sort l) (VExpr.sort l')
Tactic:
refine ⟨.sort h1, ?_, .sortDF h3⟩
State after:
case sortDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
l l' : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l
h2 : VLevel.WF U l'
h3 : l ≈ l'
⊢ HasTypeU1 env U defEq Γ✝ (VExpr.sort l') (VExpr.sort (VLevel.succ l))

State before:
case sortDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
l l' : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l
h2 : VLevel.WF U l'
h3 : l ≈ l'
⊢ HasTypeU1 env U defEq Γ✝ (VExpr.sort l') (VExpr.sort (VLevel.succ l))
Tactic:
exact .defeq (hdf (.sort (l := l'.succ) h2) (.sort (l := l.succ) h1)
  (.sortDF <| VLevel.succ_congr h3.symm)) (.sort h2)
State after:
no goals

State before:
case appDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁷ a'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁷ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝¹ :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihf :
  HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ f✝ f'✝
iha : HasTypeU1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasTypeU1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ a✝⁷ a'✝
ihBa :
  HasTypeU1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝)
⊢ HasTypeU1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasTypeU1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧ IsDefEqU1 env U hasType Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝)
Tactic:
let ⟨hf, hf', ff⟩ := ihf
State after:
case appDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁷ a'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁷ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝¹ :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihf :
  HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ f✝ f'✝
iha : HasTypeU1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasTypeU1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ a✝⁷ a'✝
ihBa :
  HasTypeU1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝)
hf : HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
hf' : HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝)
ff : IsDefEqU1 env U hasType Γ✝ f✝ f'✝
⊢ HasTypeU1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasTypeU1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧ IsDefEqU1 env U hasType Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝)

State before:
case appDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁷ a'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁷ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝¹ :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihf :
  HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ f✝ f'✝
iha : HasTypeU1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasTypeU1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ a✝⁷ a'✝
ihBa :
  HasTypeU1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝)
hf : HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
hf' : HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝)
ff : IsDefEqU1 env U hasType Γ✝ f✝ f'✝
⊢ HasTypeU1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasTypeU1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧ IsDefEqU1 env U hasType Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝)
Tactic:
let ⟨ha, ha', aa⟩ := iha
State after:
case appDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁷ a'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁷ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝¹ :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihf :
  HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ f✝ f'✝
iha : HasTypeU1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasTypeU1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ a✝⁷ a'✝
ihBa :
  HasTypeU1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝)
hf : HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
hf' : HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝)
ff : IsDefEqU1 env U hasType Γ✝ f✝ f'✝
ha : HasTypeU1 env U defEq Γ✝ a✝⁷ A✝
ha' : HasTypeU1 env U defEq Γ✝ a'✝ A✝
aa : IsDefEqU1 env U hasType Γ✝ a✝⁷ a'✝
⊢ HasTypeU1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasTypeU1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧ IsDefEqU1 env U hasType Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝)

State before:
case appDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁷ a'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁷ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝¹ :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihf :
  HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ f✝ f'✝
iha : HasTypeU1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasTypeU1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ a✝⁷ a'✝
ihBa :
  HasTypeU1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝)
hf : HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
hf' : HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝)
ff : IsDefEqU1 env U hasType Γ✝ f✝ f'✝
ha : HasTypeU1 env U defEq Γ✝ a✝⁷ A✝
ha' : HasTypeU1 env U defEq Γ✝ a'✝ A✝
aa : IsDefEqU1 env U hasType Γ✝ a✝⁷ a'✝
⊢ HasTypeU1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasTypeU1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧ IsDefEqU1 env U hasType Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝)
Tactic:
exact ⟨.app hf ha, .defeq (hdf ihBa.2.1 ihBa.1 (.symm ihBa.2.2)) (.app hf' ha'), .appDF ff aa⟩
State after:
no goals

State before:
case lamDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : 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'✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A'✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A'✝
ihB :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihB' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) B✝ B✝
ihb :
  HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) body✝ body'✝
ihb' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) body✝ body'✝
⊢ HasTypeU1 env U defEq Γ✝ (lam A✝ body✝) (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ (lam A'✝ body'✝) (VExpr.forallE A✝ B✝) ∧
      IsDefEqU1 env U hasType Γ✝ (lam A✝ body✝) (lam A'✝ body'✝)
Tactic:
refine ⟨.lam ihA.1 ihb.1, .defeq ?_ <| .lam ihA.2.1 ihb'.2.1, .lamDF ihA.2.2 ihb.2.2⟩
State after:
case lamDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : 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'✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A'✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A'✝
ihB :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihB' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) B✝ B✝
ihb :
  HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) body✝ body'✝
ihb' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) body✝ body'✝
⊢ defEq Γ✝ (VExpr.forallE A'✝ B✝) (VExpr.forallE A✝ B✝)

State before:
case lamDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : 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'✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A'✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A'✝
ihB :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihB' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) B✝ B✝
ihb :
  HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) body✝ body'✝
ihb' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) body✝ body'✝
⊢ defEq Γ✝ (VExpr.forallE A'✝ B✝) (VExpr.forallE A✝ B✝)
Tactic:
exact hdf (.forallE ihA.2.1 ihB'.1) (.forallE ihA.1 ihB.1) <|
  .symm <| .forallEDF ihA.2.2 ihB.2.2
State after:
no goals

State before:
case forallEDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A'✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A'✝
ih2 :
  HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) body'✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) body✝ body'✝
ih3 :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) body✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) body'✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) body✝ body'✝
⊢ HasTypeU1 env U defEq Γ✝ (VExpr.forallE A✝ body✝) (VExpr.sort (VLevel.imax u✝ v✝)) ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝)) ∧
      IsDefEqU1 env U hasType Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝)
Tactic:
exact ⟨.forallE ih1.1 ih2.1, .forallE ih1.2.1 ih3.2.1, .forallEDF ih1.2.2 ih2.2.2⟩
State after:
no goals

State before:
case defeqDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝² : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
ih1 :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ B✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ B✝
ih2 : HasTypeU1 env U defEq Γ✝ e1✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e2✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e1✝ e2✝
⊢ HasTypeU1 env U defEq Γ✝ e1✝ B✝ ∧ HasTypeU1 env U defEq Γ✝ e2✝ B✝ ∧ IsDefEqU1 env U hasType Γ✝ e1✝ e2✝
Tactic:
have h := hdf ih1.1 ih1.2.1 ih1.2.2
State after:
case defeqDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝² : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
ih1 :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ B✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ B✝
ih2 : HasTypeU1 env U defEq Γ✝ e1✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e2✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e1✝ e2✝
h : defEq Γ✝ A✝ B✝
⊢ HasTypeU1 env U defEq Γ✝ e1✝ B✝ ∧ HasTypeU1 env U defEq Γ✝ e2✝ B✝ ∧ IsDefEqU1 env U hasType Γ✝ e1✝ e2✝

State before:
case defeqDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝² : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
ih1 :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ B✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ B✝
ih2 : HasTypeU1 env U defEq Γ✝ e1✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e2✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e1✝ e2✝
h : defEq Γ✝ A✝ B✝
⊢ HasTypeU1 env U defEq Γ✝ e1✝ B✝ ∧ HasTypeU1 env U defEq Γ✝ e2✝ B✝ ∧ IsDefEqU1 env U hasType Γ✝ e1✝ e2✝
Tactic:
exact ⟨.defeq h ih2.1, .defeq h ih2.2.1, ih2.2.2⟩
State after:
no goals

State before:
case beta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝¹ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihe :
  HasTypeU1 env U defEq (A✝ :: Γ✝) e✝ B✝ ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) e✝ B✝ ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) e✝ e✝
ihe' : HasTypeU1 env U defEq Γ✝ e'✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e'✝ e'✝
a_ih✝ :
  HasTypeU1 env U defEq Γ✝ (inst B✝ e'✝) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst B✝ e'✝) (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType Γ✝ (inst B✝ e'✝) (inst B✝ e'✝)
ihee :
  HasTypeU1 env U defEq Γ✝ (inst e✝ e'✝) (inst B✝ e'✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst e✝ e'✝) (inst B✝ e'✝) ∧ IsDefEqU1 env U hasType Γ✝ (inst e✝ e'✝) (inst e✝ e'✝)
⊢ HasTypeU1 env U defEq Γ✝ (app (lam A✝ e✝) e'✝) (inst B✝ e'✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst e✝ e'✝) (inst B✝ e'✝) ∧
      IsDefEqU1 env U hasType Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝)
Tactic:
exact ⟨.app (.lam ihA.1 ihe.1) ihe'.1, ihee.1, .beta (hty ihe.1) (hty ihe'.1)⟩
State after:
no goals

State before:
case eta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : 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✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝¹ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
a_ih✝ :
  HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
      IsDefEqU1 env U hasType (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1)
ihe :
  HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ e✝ e✝
ihe' :
  HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
      IsDefEqU1 env U hasType (A✝ :: Γ✝) (lift e✝) (lift e✝)
⊢ HasTypeU1 env U defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
      IsDefEqU1 env U hasType Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝
Tactic:
have := HasTypeU1.app ihe'.1 (.bvar .zero)
State after:
case eta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : 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✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝¹ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
a_ih✝ :
  HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
      IsDefEqU1 env U hasType (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1)
ihe :
  HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ e✝ e✝
ihe' :
  HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
      IsDefEqU1 env U hasType (A✝ :: Γ✝) (lift e✝) (lift e✝)
this : HasTypeU1 env U defEq (A✝ :: Γ✝) (app (lift e✝) (VExpr.bvar 0)) (inst (liftN 1 B✝ 1) (VExpr.bvar 0))
⊢ HasTypeU1 env U defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
      IsDefEqU1 env U hasType Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝

State before:
case eta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : 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✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝¹ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
a_ih✝ :
  HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
      IsDefEqU1 env U hasType (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1)
ihe :
  HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ e✝ e✝
ihe' :
  HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
      IsDefEqU1 env U hasType (A✝ :: Γ✝) (lift e✝) (lift e✝)
this : HasTypeU1 env U defEq (A✝ :: Γ✝) (app (lift e✝) (VExpr.bvar 0)) (inst (liftN 1 B✝ 1) (VExpr.bvar 0))
⊢ HasTypeU1 env U defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
      IsDefEqU1 env U hasType Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝
Tactic:
rw [instN_bvar0] at this
State after:
case eta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : 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✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝¹ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
a_ih✝ :
  HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
      IsDefEqU1 env U hasType (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1)
ihe :
  HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ e✝ e✝
ihe' :
  HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
      IsDefEqU1 env U hasType (A✝ :: Γ✝) (lift e✝) (lift e✝)
this : HasTypeU1 env U defEq (A✝ :: Γ✝) (app (lift e✝) (VExpr.bvar 0)) B✝
⊢ HasTypeU1 env U defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
      IsDefEqU1 env U hasType Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝

State before:
case eta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : 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✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝¹ :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
a_ih✝ :
  HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
      IsDefEqU1 env U hasType (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1)
ihe :
  HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ e✝ e✝
ihe' :
  HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
      IsDefEqU1 env U hasType (A✝ :: Γ✝) (lift e✝) (lift e✝)
this : HasTypeU1 env U defEq (A✝ :: Γ✝) (app (lift e✝) (VExpr.bvar 0)) B✝
⊢ HasTypeU1 env U defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
      IsDefEqU1 env U hasType Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝
Tactic:
exact ⟨.lam ihA.1 this, ihe.1, .eta⟩
State after:
no goals

State before:
case proofIrrel
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEqStrong env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
ih1 :
  HasTypeU1 env U defEq Γ✝ p✝ (VExpr.sort VLevel.zero) ∧
    HasTypeU1 env U defEq Γ✝ p✝ (VExpr.sort VLevel.zero) ∧ IsDefEqU1 env U hasType Γ✝ p✝ p✝
ih2 : HasTypeU1 env U defEq Γ✝ h✝ p✝ ∧ HasTypeU1 env U defEq Γ✝ h✝ p✝ ∧ IsDefEqU1 env U hasType Γ✝ h✝ h✝
ih3 : HasTypeU1 env U defEq Γ✝ h'✝ p✝ ∧ HasTypeU1 env U defEq Γ✝ h'✝ p✝ ∧ IsDefEqU1 env U hasType Γ✝ h'✝ h'✝
⊢ HasTypeU1 env U defEq Γ✝ h✝ p✝ ∧ HasTypeU1 env U defEq Γ✝ h'✝ p✝ ∧ IsDefEqU1 env U hasType Γ✝ h✝ h'✝
Tactic:
exact ⟨ih2.1, ih3.1, .proofIrrel (hty ih1.1) (hty ih2.1) (hty ih3.1)⟩
State after:
no goals

State before:
case extra
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (VExpr.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✝² :
  HasTypeU1 env U defEq [] (VExpr.instL ls✝ df✝.type) (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq [] (VExpr.instL ls✝ df✝.type) (VExpr.sort u✝) ∧
      IsDefEqU1 env U hasType [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type)
a_ih✝¹ :
  HasTypeU1 env U defEq [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
    HasTypeU1 env U defEq [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEqU1 env U hasType [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs)
a_ih✝ :
  HasTypeU1 env U defEq [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
    HasTypeU1 env U defEq [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEqU1 env U hasType [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs)
ihl' :
  HasTypeU1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEqU1 env U hasType Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs)
ihr' :
  HasTypeU1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEqU1 env U hasType Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs)
⊢ HasTypeU1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEqU1 env U hasType Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs)
Tactic:
exact ⟨ihl'.1, ihr'.1, .extra h1 h2 h3⟩
State after:
no goals