Let X, Tx, seq and x be given.
Assume Hconv: converges_to X Tx seq x.
We prove the intermediate claim Hseq: sequence_on seq X.
An exact proof term for the current goal is (converges_to_sequence_on X Tx seq x Hconv).
We prove the intermediate claim Hneton: net_converges_on X Tx (sequence_as_net seq) ω (inclusion_rel ω) x.
An exact proof term for the current goal is (iffEL (converges_to X Tx seq x) (net_converges_on X Tx (sequence_as_net seq) ω (inclusion_rel ω) x) (converges_to_iff_net_converges_on_sequence_as_net X Tx seq x Hseq) Hconv).
An exact proof term for the current goal is (net_converges_on_implies_net_converges X Tx (sequence_as_net seq) ω (inclusion_rel ω) x Hneton).
∎