Let J, a and b be given.
Assume Hab: (a,b) ∈ rev_inclusion_rel J.
We prove the intermediate claim Hab': (a,b) ∈ {p ∈ setprod J J|p 1 ⊆ p 0}.
rewrite the current goal using (rev_inclusion_rel_def J) (from right to left).
An exact proof term for the current goal is Hab.
We prove the intermediate claim Hprod: (a,b) ∈ setprod J J.
An exact proof term for the current goal is (SepE1 (setprod J J) (λp : set ⇒ p 1 ⊆ p 0) (a,b) Hab').
We prove the intermediate claim Hsub: (a,b) 1 ⊆ (a,b) 0.
An exact proof term for the current goal is (SepE2 (setprod J J) (λp : set ⇒ p 1 ⊆ p 0) (a,b) Hab').
Apply andI to the current goal.
An exact proof term for the current goal is Hprod.
We will prove b ⊆ a.
Let y be given.
Assume Hy: y ∈ b.
We will prove y ∈ a.
We prove the intermediate claim Hy1: y ∈ (a,b) 1.
rewrite the current goal using (tuple_2_1_eq a b) (from left to right).
An exact proof term for the current goal is Hy.
We prove the intermediate claim Hy0: y ∈ (a,b) 0.
An exact proof term for the current goal is (Hsub y Hy1).
rewrite the current goal using (tuple_2_0_eq a b) (from right to left).
An exact proof term for the current goal is Hy0.
∎