apply dite (j.1 = k) <;> apply dite (i.1 = k) <;> intro hik hjk
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]
case t.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case t.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.t
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]

case e.e
n : Nat
x : Permutation n
i j : Fin n
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then if ↑j = ↑i then x[↑i] else x[↑j]
    else if ↑i = k then x[↑i] else if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) =
    x[k]