α : Sort u_1
ctx : Context α
a b : Expr
h✝ : (norm ctx a == norm ctx b) = true
h : evalList α ctx (norm ctx a) = evalList α ctx (norm ctx b)
⊢ eval α ctx a = eval α ctx b
α : Sort u_1
ctx : Context α
a b : Expr
h : (norm ctx a == norm ctx b) = true
⊢ eval α ctx a = eval α ctx b
have h := congrArg (evalList α ctx) (eq_of_beq h)
α : Sort u_1
ctx : Context α
a b : Expr
h✝ : (norm ctx a == norm ctx b) = true
h : eval α ctx a = eval α ctx b
⊢ eval α ctx a = eval α ctx b
α : Sort u_1
ctx : Context α
a b : Expr
h✝ : (norm ctx a == norm ctx b) = true
h : evalList α ctx (norm ctx a) = evalList α ctx (norm ctx b)
⊢ eval α ctx a = eval α ctx b
rw [eval_norm, eval_norm] at h
no goals
α : Sort u_1
ctx : Context α
a b : Expr
h✝ : (norm ctx a == norm ctx b) = true
h : eval α ctx a = eval α ctx b
⊢ eval α ctx a = eval α ctx b
assumption