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

State before:
TY : Typing
Γ : List VExpr
e1 e2 e3 : VExpr
H1 : NormalEq TY Γ e1 e2
H2 : NormalEq TY Γ e2 e3
⊢ NormalEq TY Γ e1 e3
Tactic:
sorry
State after:
no goals