Let K, le, i and j be given.
Assume Hij: (i,j) ∈ {q ∈ setprod K K|(q 1) 0 ⊆ (q 0) 0 ∧ ((q 0) 1,(q 1) 1) ∈ le}.
We prove the intermediate claim Hraw: ((i,j) 1) 0 ⊆ ((i,j) 0) 0 ∧ (((i,j) 0) 1,((i,j) 1) 1) ∈ le.
An exact proof term for the current goal is (SepE2 (setprod K K) (λq : set ⇒ (q 1) 0 ⊆ (q 0) 0 ∧ ((q 0) 1,(q 1) 1) ∈ le) (i,j) Hij).
Apply andI to the current goal.
Let y be given.
Assume Hy: y ∈ (j 0).
We will prove y ∈ (i 0).
We prove the intermediate claim Hsub: ((i,j) 1) 0 ⊆ ((i,j) 0) 0.
An exact proof term for the current goal is (andEL (((i,j) 1) 0 ⊆ ((i,j) 0) 0) ((((i,j) 0) 1,((i,j) 1) 1) ∈ le) Hraw).
We prove the intermediate claim Hy1: y ∈ (((i,j) 1) 0).
rewrite the current goal using (tuple_2_1_eq i j) (from left to right).
An exact proof term for the current goal is Hy.
We prove the intermediate claim Hy0: y ∈ (((i,j) 0) 0).
An exact proof term for the current goal is (Hsub y Hy1).
rewrite the current goal using (tuple_2_0_eq i j) (from right to left).
An exact proof term for the current goal is Hy0.
We prove the intermediate claim Hle: (((i,j) 0) 1,((i,j) 1) 1) ∈ le.
An exact proof term for the current goal is (andER (((i,j) 1) 0 ⊆ ((i,j) 0) 0) ((((i,j) 0) 1,((i,j) 1) 1) ∈ le) Hraw).
We prove the intermediate claim Hi1: ((i,j) 0) 1 = (i 1).
rewrite the current goal using (tuple_2_0_eq i j) (from left to right).
Use reflexivity.
We prove the intermediate claim Hj1: ((i,j) 1) 1 = (j 1).
rewrite the current goal using (tuple_2_1_eq i j) (from left to right).
Use reflexivity.
rewrite the current goal using Hi1 (from right to left).
rewrite the current goal using Hj1 (from right to left).
An exact proof term for the current goal is Hle.
∎