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

State before:
env : VEnv
U : Nat
Γ : List VExpr
V A B : VExpr
henv : Ordered env
H : HasType env U Γ (forallE A B) V
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
refine H.forallE_inv' henv ?_ (.inl rfl)
State after:
env : VEnv
U : Nat
Γ : List VExpr
V A B : VExpr
henv : Ordered env
H : HasType env U Γ (forallE A B) V
⊢ OnTypes env fun U e x => ∀ (A B : VExpr), e = forallE A B → IsType env U [] A ∧ IsType env U [A] B

State before:
env : VEnv
U : Nat
Γ : List VExpr
V A B : VExpr
henv : Ordered env
H : HasType env U Γ (forallE A B) V
⊢ OnTypes env fun U e x => ∀ (A B : VExpr), e = forallE A B → IsType env U [] A ∧ IsType env U [A] B
Tactic:
exact henv.induction
  (fun env U e _ => ∀ A B, e = forallE A B → IsType env U [] A ∧ IsType env U [A] B)
  (fun le H A B eq => (H A B eq).imp (.mono le) (.mono le))
  (fun henv IH H A B eq => H.forallE_inv' henv IH (.inl eq))
State after:
no goals