Lean4
/-- Cast `e : te[p/x, rfl/h, ...]` to `h ▸ e : te`. -/
def castFwd (e te p x h : Expr) (Δ : Array (FVarId × Expr)) (δ : Std.HashSet FVarId) : MetaM Expr := do
if !te.hasAnyFVar (fun f => f == x.fvarId! || f == h.fvarId! || Δ.any (·.1 == f) || δ.contains f) then
return e
let motive ←
do
withLocalDeclD `x' (← inferType x) fun x' => do
withLocalDeclD `h' (← mkEq p x') fun h' => do
let te ← zetaDelta te δ
let mut fs := #[x, h]
let mut es := #[x', h']
for (f, M) in Δ do
fs := fs.push (.fvar f)
es := es.push (← mkEqRec M (.fvar f) (← mkEqTrans (← mkEqSymm h) h'))
let te := te.replaceFVars fs es
mkLambdaFVars #[x', h'] te
let e' ← mkEqRec motive e h
trace[Tactic.depRewrite.cast]"casting (p ↦ x):{indentExpr e'}"
return e'
