Let J, a and b be given.

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

Assume Hsub: b ⊆ a.

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

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

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

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

Let y be given.

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

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

We prove the intermediate claim Hyb: y ∈ b.

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

An exact proof term for the current goal is Hy.

We prove the intermediate claim Hya: y ∈ a.

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

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

An exact proof term for the current goal is Hya.

∎