Let X, n, F, e and x be given.
Assume HnO: n ∈ ω.
Assume HxX: x ∈ X.
Assume HtermUI: ∀k : set, k ∈ ordsucc n → apply_fun (apply_fun e k) x ∈ unit_interval.
Assume Hlast0: apply_fun (apply_fun e n) x = 0.
Assume Hbij: bijection (ordsucc n) F e.
We will prove bijection n (F ∖ {apply_fun e n}) e ∧ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc 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_drop_last n F e HnO Hbij).
An exact proof term for the current goal is (nat_primrec_sum_S_drop_zero_unit_interval X n e x HnO HxX HtermUI Hlast0).
∎