Let X, x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
We will prove ∃p : set, path_between X x y p.
Set p to be the term {(t,If_i (t = 0) x y)|t ∈ unit_interval}.
We use p to witness the existential quantifier.
We will prove path_between X x y p.
We will prove function_on p unit_interval X ∧ apply_fun p 0 = x ∧ apply_fun p 1 = y.
Apply andI to the current goal.
Apply andI to the current goal.
Let t be given.
Assume HtI: t ∈ unit_interval.
We will prove apply_fun p t ∈ X.
We prove the intermediate claim Happ: apply_fun p t = If_i (t = 0) x y.
We will prove apply_fun p t = If_i (t = 0) x y.
We will prove Eps_i (λu : set ⇒ (t,u) ∈ p) = If_i (t = 0) x y.
We prove the intermediate claim Hpair: (t,If_i (t = 0) x y) ∈ p.
An exact proof term for the current goal is (ReplI unit_interval (λt0 : set ⇒ (t0,If_i (t0 = 0) x y)) t HtI).
We prove the intermediate claim Heps: (t,Eps_i (λu : set ⇒ (t,u) ∈ p)) ∈ p.
An exact proof term for the current goal is (Eps_i_ax (λu : set ⇒ (t,u) ∈ p) (If_i (t = 0) x y) Hpair).
Apply (ReplE_impred unit_interval (λt0 : set ⇒ (t0,If_i (t0 = 0) x y)) (t,Eps_i (λu : set ⇒ (t,u) ∈ p)) Heps (Eps_i (λu : set ⇒ (t,u) ∈ p) = If_i (t = 0) x y)) to the current goal.
Let t0 be given.
Assume Ht0: t0 ∈ unit_interval.
Assume Heq: (t,Eps_i (λu : set ⇒ (t,u) ∈ p)) = (t0,If_i (t0 = 0) x y).
We prove the intermediate claim Ht_eq: t = t0.
rewrite the current goal using (tuple_2_0_eq t (Eps_i (λu : set ⇒ (t,u) ∈ p))) (from right to left).
rewrite the current goal using (tuple_2_0_eq t0 (If_i (t0 = 0) x y)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hu_eq: Eps_i (λu : set ⇒ (t,u) ∈ p) = If_i (t0 = 0) x y.
rewrite the current goal using (tuple_2_1_eq t (Eps_i (λu : set ⇒ (t,u) ∈ p))) (from right to left).
rewrite the current goal using (tuple_2_1_eq t0 (If_i (t0 = 0) x y)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
rewrite the current goal using Hu_eq (from left to right).
rewrite the current goal using Ht_eq (from right to left).
Use reflexivity.
rewrite the current goal using Happ (from left to right).
Apply (xm (t = 0)) to the current goal.
Assume Ht0: t = 0.
rewrite the current goal using (If_i_1 (t = 0) x y Ht0) (from left to right).
An exact proof term for the current goal is HxX.
Assume Hnt0: ¬ (t = 0).
rewrite the current goal using (If_i_0 (t = 0) x y Hnt0) (from left to right).
An exact proof term for the current goal is HyX.
We prove the intermediate claim H01: 0 ∈ unit_interval ∧ 1 ∈ unit_interval.
An exact proof term for the current goal is zero_one_in_unit_interval.
We prove the intermediate claim H0I: 0 ∈ unit_interval.
An exact proof term for the current goal is (andEL (0 ∈ unit_interval) (1 ∈ unit_interval) H01).
We prove the intermediate claim Happ0: apply_fun p 0 = If_i (0 = 0) x y.
We will prove apply_fun p 0 = If_i (0 = 0) x y.
We will prove Eps_i (λu : set ⇒ (0,u) ∈ p) = If_i (0 = 0) x y.
We prove the intermediate claim Hpair: (0,If_i (0 = 0) x y) ∈ p.
An exact proof term for the current goal is (ReplI unit_interval (λt0 : set ⇒ (t0,If_i (t0 = 0) x y)) 0 H0I).
We prove the intermediate claim Heps: (0,Eps_i (λu : set ⇒ (0,u) ∈ p)) ∈ p.
An exact proof term for the current goal is (Eps_i_ax (λu : set ⇒ (0,u) ∈ p) (If_i (0 = 0) x y) Hpair).
Apply (ReplE_impred unit_interval (λt0 : set ⇒ (t0,If_i (t0 = 0) x y)) (0,Eps_i (λu : set ⇒ (0,u) ∈ p)) Heps (Eps_i (λu : set ⇒ (0,u) ∈ p) = If_i (0 = 0) x y)) to the current goal.
Let t0 be given.
Assume Ht0: t0 ∈ unit_interval.
Assume Heq: (0,Eps_i (λu : set ⇒ (0,u) ∈ p)) = (t0,If_i (t0 = 0) x y).
We prove the intermediate claim Ht_eq: 0 = t0.
rewrite the current goal using (tuple_2_0_eq 0 (Eps_i (λu : set ⇒ (0,u) ∈ p))) (from right to left).
rewrite the current goal using (tuple_2_0_eq t0 (If_i (t0 = 0) x y)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hu_eq: Eps_i (λu : set ⇒ (0,u) ∈ p) = If_i (t0 = 0) x y.
rewrite the current goal using (tuple_2_1_eq 0 (Eps_i (λu : set ⇒ (0,u) ∈ p))) (from right to left).
rewrite the current goal using (tuple_2_1_eq t0 (If_i (t0 = 0) x y)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
rewrite the current goal using Hu_eq (from left to right).
rewrite the current goal using Ht_eq (from right to left).
Use reflexivity.
rewrite the current goal using Happ0 (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) x y H00) (from left to right).
Use reflexivity.
We prove the intermediate claim H01: 0 ∈ unit_interval ∧ 1 ∈ unit_interval.
An exact proof term for the current goal is zero_one_in_unit_interval.
We prove the intermediate claim H1I: 1 ∈ unit_interval.
An exact proof term for the current goal is (andER (0 ∈ unit_interval) (1 ∈ unit_interval) H01).
We prove the intermediate claim Happ1: apply_fun p 1 = If_i (1 = 0) x y.
We will prove apply_fun p 1 = If_i (1 = 0) x y.
We will prove Eps_i (λu : set ⇒ (1,u) ∈ p) = If_i (1 = 0) x y.
We prove the intermediate claim Hpair: (1,If_i (1 = 0) x y) ∈ p.
An exact proof term for the current goal is (ReplI unit_interval (λt0 : set ⇒ (t0,If_i (t0 = 0) x y)) 1 H1I).
We prove the intermediate claim Heps: (1,Eps_i (λu : set ⇒ (1,u) ∈ p)) ∈ p.
An exact proof term for the current goal is (Eps_i_ax (λu : set ⇒ (1,u) ∈ p) (If_i (1 = 0) x y) Hpair).
Apply (ReplE_impred unit_interval (λt0 : set ⇒ (t0,If_i (t0 = 0) x y)) (1,Eps_i (λu : set ⇒ (1,u) ∈ p)) Heps (Eps_i (λu : set ⇒ (1,u) ∈ p) = If_i (1 = 0) x y)) to the current goal.
Let t0 be given.
Assume Ht0: t0 ∈ unit_interval.
Assume Heq: (1,Eps_i (λu : set ⇒ (1,u) ∈ p)) = (t0,If_i (t0 = 0) x y).
We prove the intermediate claim Ht_eq: 1 = t0.
rewrite the current goal using (tuple_2_0_eq 1 (Eps_i (λu : set ⇒ (1,u) ∈ p))) (from right to left).
rewrite the current goal using (tuple_2_0_eq t0 (If_i (t0 = 0) x y)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hu_eq: Eps_i (λu : set ⇒ (1,u) ∈ p) = If_i (t0 = 0) x y.
rewrite the current goal using (tuple_2_1_eq 1 (Eps_i (λu : set ⇒ (1,u) ∈ p))) (from right to left).
rewrite the current goal using (tuple_2_1_eq t0 (If_i (t0 = 0) x y)) (from right to left).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
rewrite the current goal using Hu_eq (from left to right).
rewrite the current goal using Ht_eq (from right to left).
Use reflexivity.
rewrite the current goal using Happ1 (from left to right).
We prove the intermediate claim Hneq: ¬ (1 = 0).
Assume H10: 1 = 0.
Apply neq_0_1 to the current goal.
rewrite the current goal using H10 (from left to right).
Use reflexivity.
rewrite the current goal using (If_i_0 (1 = 0) x y Hneq) (from left to right).
Use reflexivity.
∎