Theorem: Lean4Lean.NormalEq.symm (Lean4Lean/Theory/Typing/ParallelReduction.lean)

State before:
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
H : NormalEq TY Γ e1 e2
⊢ NormalEq TY Γ e2 e1
Tactic:
induction H with
| refl h => exact .refl h
| sortDF h1 h2 h3 => exact .sortDF h2 h1 h3.symm
| appDF h1 h2 h3 h4 _ _ ih1 ih2 => exact .appDF h2 h1 h4 h3 ih1 ih2
| lamDF h1 h2 _ _ ih1 ih2 => exact .lamDF h1 (TY.trans ih1.defeq h2) ih1 ih2
| forallEDF h1 h2 _ h4 h5 ih1 ih2 =>
  exact .forallEDF h1 (TY.trans ih1.defeq h2) ih1 (TY.defeq_l h5.defeq h4) ih2
| etaL h1 _ ih => exact .etaR h1 ih
| etaR h1 _ ih => exact .etaL h1 ih
| proofIrrel h1 h2 h3 => exact .proofIrrel h1 h3 h2
State after:
no goals

State before:
case refl
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
e✝ A✝ : VExpr
h : TY.HasType Γ✝ e✝ A✝
⊢ NormalEq TY Γ✝ e✝ e✝
Tactic:
exact .refl h
State after:
no goals

State before:
case sortDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
l₁✝ l₂✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF TY.univs l₁✝
h2 : VLevel.WF TY.univs l₂✝
h3 : l₁✝ ≈ l₂✝
⊢ NormalEq TY Γ✝ (sort l₂✝) (sort l₁✝)
Tactic:
exact .sortDF h2 h1 h3.symm
State after:
no goals

State before:
case appDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
f₁✝ A✝ B✝ f₂✝ a₁✝ a₂✝ : VExpr
h1 : TY.HasType Γ✝ f₁✝ (forallE A✝ B✝)
h2 : TY.HasType Γ✝ f₂✝ (forallE A✝ B✝)
h3 : TY.HasType Γ✝ a₁✝ A✝
h4 : TY.HasType Γ✝ a₂✝ A✝
a✝¹ : NormalEq TY Γ✝ f₁✝ f₂✝
a✝ : NormalEq TY Γ✝ a₁✝ a₂✝
ih1 : NormalEq TY Γ✝ f₂✝ f₁✝
ih2 : NormalEq TY Γ✝ a₂✝ a₁✝
⊢ NormalEq TY Γ✝ (app f₂✝ a₂✝) (app f₁✝ a₁✝)
Tactic:
exact .appDF h2 h1 h4 h3 ih1 ih2
State after:
no goals

State before:
case lamDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ body₁✝ body₂✝ : VExpr
h1 : TY.HasType Γ✝ A✝ (sort u✝)
h2 : TY.IsDefEq Γ✝ A₁✝ A✝
a✝¹ : NormalEq TY Γ✝ A₁✝ A₂✝
a✝ : NormalEq TY (A✝ :: Γ✝) body₁✝ body₂✝
ih1 : NormalEq TY Γ✝ A₂✝ A₁✝
ih2 : NormalEq TY (A✝ :: Γ✝) body₂✝ body₁✝
⊢ NormalEq TY Γ✝ (lam A₂✝ body₂✝) (lam A₁✝ body₁✝)
Tactic:
exact .lamDF h1 (TY.trans ih1.defeq h2) ih1 ih2
State after:
no goals

State before:
case forallEDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
A₁✝ A₂✝ B₁✝ : VExpr
v✝ : VLevel
B₂✝ : VExpr
h1 : TY.HasType Γ✝ A✝ (sort u✝)
h2 : TY.IsDefEq Γ✝ A₁✝ A✝
a✝ : NormalEq TY Γ✝ A₁✝ A₂✝
h4 : TY.HasType (A✝ :: Γ✝) B₁✝ (sort v✝)
h5 : NormalEq TY (A✝ :: Γ✝) B₁✝ B₂✝
ih1 : NormalEq TY Γ✝ A₂✝ A₁✝
ih2 : NormalEq TY (A✝ :: Γ✝) B₂✝ B₁✝
⊢ NormalEq TY Γ✝ (forallE A₂✝ B₂✝) (forallE A₁✝ B₁✝)
Tactic:
exact .forallEDF h1 (TY.trans ih1.defeq h2) ih1 (TY.defeq_l h5.defeq h4) ih2
State after:
no goals

State before:
case etaL
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
ih : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
⊢ NormalEq TY Γ✝ e'✝ (lam A✝ e✝)
Tactic:
exact .etaR h1 ih
State after:
no goals

State before:
case etaR
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
e'✝ A✝ B✝ e✝ : VExpr
h1 : TY.HasType Γ✝ e'✝ (forallE A✝ B✝)
a✝ : NormalEq TY (A✝ :: Γ✝) (app (lift e'✝) (bvar 0)) e✝
ih : NormalEq TY (A✝ :: Γ✝) e✝ (app (lift e'✝) (bvar 0))
⊢ NormalEq TY Γ✝ (lam A✝ e✝) e'✝
Tactic:
exact .etaL h1 ih
State after:
no goals

State before:
case proofIrrel
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
env : VEnv
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
h1 : TY.HasType Γ✝ p✝ (sort VLevel.zero)
h2 : TY.HasType Γ✝ h✝ p✝
h3 : TY.HasType Γ✝ h'✝ p✝
⊢ NormalEq TY Γ✝ h'✝ h✝
Tactic:
exact .proofIrrel h1 h3 h2
State after:
no goals