Theorem: Lean4Lean.VEnv.DefInv.symm (Lean4Lean/Theory/Typing/Stratified.lean)

State before:
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 : VExpr
h : DefInv env U Γ e1 e2
⊢ DefInv env U Γ e2 e1
Tactic:
cases e1 <;> cases e2 <;> try trivial
State after:
case sort.sort
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
u✝¹ u✝ : VLevel
h : DefInv env U Γ (sort u✝¹) (sort u✝)
⊢ DefInv env U Γ (sort u✝) (sort u✝¹)

case forallE.forallE
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (forallE binderType✝ body✝)
⊢ DefInv env U Γ (forallE binderType✝ body✝) (forallE binderType✝¹ body✝¹)

State before:
case forallE.lam
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (lam binderType✝ body✝)
⊢ DefInv env U Γ (lam binderType✝ body✝) (forallE binderType✝¹ body✝¹)
Tactic:
trivial
State after:
no goals

State before:
case sort.sort
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
u✝¹ u✝ : VLevel
h : DefInv env U Γ (sort u✝¹) (sort u✝)
⊢ DefInv env U Γ (sort u✝) (sort u✝¹)
Tactic:
exact h.symm
State after:
no goals

State before:
case forallE.forallE
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (forallE binderType✝ body✝)
⊢ DefInv env U Γ (forallE binderType✝ body✝) (forallE binderType✝¹ body✝¹)
Tactic:
let ⟨u, v, h1, h2⟩ := h
State after:
case forallE.forallE
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (forallE binderType✝ body✝)
u v : VLevel
h1 : IsDefEq env U Γ binderType✝¹ binderType✝ (sort u)
h2 : IsDefEq env U (binderType✝¹ :: Γ) body✝¹ body✝ (sort v)
⊢ DefInv env U Γ (forallE binderType✝ body✝) (forallE binderType✝¹ body✝¹)

State before:
case forallE.forallE
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (forallE binderType✝ body✝)
u v : VLevel
h1 : IsDefEq env U Γ binderType✝¹ binderType✝ (sort u)
h2 : IsDefEq env U (binderType✝¹ :: Γ) body✝¹ body✝ (sort v)
⊢ DefInv env U Γ (forallE binderType✝ body✝) (forallE binderType✝¹ body✝¹)
Tactic:
exact ⟨u, v, h1.symm, h1.defeqDF_l henv h2.symm⟩
State after:
no goals