def LeanSubst.Nat.rmap {T : Type u2} (r : Ren T) : Nat → Nat

Equations

• LeanSubst.Nat.rmap r x✝ = r.act x✝

@[instance_reducible]

instance LeanSubst.instRenMapNatConsNil {T : Type u2} : RenMap Nat [T]

Equations

• LeanSubst.instRenMapNatConsNil = { rmap := fun (r : LeanSubst.RenVec [T]) => LeanSubst.Nat.rmap r.fst }

@[simp]

theorem LeanSubst.Nat.rmap_simp {T : Type u2} {r : Ren T} {n : Nat} : n⟨r⟩ = r.act n