namespace Mt.Utils.Fin

def 
cast: {n m : Nat} → Fin n → n = m → Fin m
cast {
n: Nat
n 
m: Nat
m : 
Nat: Type
Nat} (
i: Fin n
i : 
Fin: Nat → Type
Fin 
n: Nat
n) (
eq: n = m
eq : 
n: Nat
n = 
m: Nat
m) : 
Fin: Nat → Type
Fin 
m: Nat
m :=⟨
i: Fin n
i.
val: {n : Nat} → Fin n → Nat
val, calc
  
i: Fin n
i.
val: {n : Nat} → Fin n → Nat
val < 
n: Nat
n :=
i: Fin n
i.
isLt: ∀ {n : Nat} (self : Fin n), self.val < n
isLt
      
n: Nat
n = 
m: Nat
m :=
eq: n = m
eq⟩

end Mt.Utils.Fin