Let X, n, F, e, i and x be given.

Assume HnO: n ∈ ω.

Assume HiN: i ∈ n.

Assume HsiN: ordsucc i ∈ n.

Assume HxX: x ∈ X.

Assume Hbij: bijection n F e.

Assume HtermUI: ∀k : set, k ∈ n → apply_fun (apply_fun e k) x ∈ unit_interval.

We will prove bijection n F (swap_adjacent e i n) ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun (swap_adjacent e i n) k) x)) n = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) n.

Apply andI to the current goal.

An exact proof term for the current goal is (bijection_swap_adjacent F e i n HiN HsiN Hbij).

An exact proof term for the current goal is (nat_primrec_sum_swap_adjacent_unit_interval X n e i x HnO HiN HsiN HxX HtermUI).

∎