Let f be given.
Assume Hf: f ∈ real_sequences.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ Romega_clipped_diffs f f.
We will prove a ∈ {0}.
Apply (ReplE_impred ω (λn : set ⇒ Romega_coord_clipped_diff f f n) a Ha (a ∈ {0})) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume Han: a = Romega_coord_clipped_diff f f n.
rewrite the current goal using Han (from left to right).
We prove the intermediate claim Hz: Romega_coord_clipped_diff f f n = 0.
An exact proof term for the current goal is (Romega_coord_clipped_diff_self_zero f n Hf HnO).
rewrite the current goal using Hz (from left to right).
An exact proof term for the current goal is (SingI 0).
Let a be given.
Assume Ha0: a ∈ {0}.
We will prove a ∈ Romega_clipped_diffs f f.
We prove the intermediate claim HaEq: a = 0.
An exact proof term for the current goal is (SingE 0 a Ha0).
rewrite the current goal using HaEq (from left to right).
We will prove 0 ∈ Romega_clipped_diffs f f.
We prove the intermediate claim H0O: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Hdef: 0 = Romega_coord_clipped_diff f f 0.
rewrite the current goal using (Romega_coord_clipped_diff_self_zero f 0 Hf H0O) (from left to right).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (ReplI ω (λn : set ⇒ Romega_coord_clipped_diff f f n) 0 H0O).
∎