Let t be given.
Assume Ht: t ∈ unit_interval.
We will prove apply_fun flip_unit_interval t = add_SNo 1 (minus_SNo t).
We will prove Eps_i (λz ⇒ (t,z) ∈ flip_unit_interval) = add_SNo 1 (minus_SNo t).
We prove the intermediate claim H1: (t,add_SNo 1 (minus_SNo t)) ∈ flip_unit_interval.
An exact proof term for the current goal is (ReplI unit_interval (λt0 : set ⇒ (t0,add_SNo 1 (minus_SNo t0))) t Ht).
We prove the intermediate claim H2: (t,Eps_i (λz ⇒ (t,z) ∈ flip_unit_interval)) ∈ flip_unit_interval.
An exact proof term for the current goal is (Eps_i_ax (λz ⇒ (t,z) ∈ flip_unit_interval) (add_SNo 1 (minus_SNo t)) H1).
Apply (ReplE_impred unit_interval (λt0 : set ⇒ (t0,add_SNo 1 (minus_SNo t0))) (t,Eps_i (λz ⇒ (t,z) ∈ flip_unit_interval)) H2) to the current goal.
Let y be given.
Assume Hy: y ∈ unit_interval.
Assume Heq: (t,Eps_i (λz ⇒ (t,z) ∈ flip_unit_interval)) = (y,add_SNo 1 (minus_SNo y)).
We prove the intermediate claim Ht_eq: t = y.
rewrite the current goal using (tuple_2_0_eq t (Eps_i (λz ⇒ (t,z) ∈ flip_unit_interval))) (from right to left).
rewrite the current goal using (tuple_2_0_eq y (add_SNo 1 (minus_SNo y))) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hz_eq: Eps_i (λz ⇒ (t,z) ∈ flip_unit_interval) = add_SNo 1 (minus_SNo y).
rewrite the current goal using (tuple_2_1_eq t (Eps_i (λz ⇒ (t,z) ∈ flip_unit_interval))) (from right to left).
rewrite the current goal using (tuple_2_1_eq y (add_SNo 1 (minus_SNo y))) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
rewrite the current goal using Hz_eq (from left to right).
rewrite the current goal using Ht_eq (from right to left).
Use reflexivity.
∎