Let J, a and b be given.

Assume Hprod: (a,b) ∈ setprod J J.

Assume Hsub: a ⊆ b.

We will prove (a,b) ∈ inclusion_rel J.

rewrite the current goal using (inclusion_rel_def J) (from left to right).

Apply (SepI (setprod J J) (λp : set ⇒ (p 0) ⊆ (p 1)) (a,b) Hprod) to the current goal.

We will prove (a,b) 0 ⊆ (a,b) 1.

Let y be given.

Assume Hy: y ∈ (a,b) 0.

We will prove y ∈ (a,b) 1.

We prove the intermediate claim Hya: y ∈ a.

rewrite the current goal using (tuple_2_0_eq a b) (from right to left).

An exact proof term for the current goal is Hy.

We prove the intermediate claim Hyb: y ∈ b.

An exact proof term for the current goal is (Hsub y Hya).

rewrite the current goal using (tuple_2_1_eq a b) (from left to right).

An exact proof term for the current goal is Hyb.

∎