Let K1, le1, K2, le2, a and b be given.
Assume Hab: (a,b) ∈ setprod_le K1 le1 K2 le2.
We prove the intermediate claim Hraw: (((a,b) 0) 0,((a,b) 1) 0) ∈ le1 ∧ (((a,b) 0) 1,((a,b) 1) 1) ∈ le2.
An exact proof term for the current goal is (SepE2 (setprod (setprod K1 K2) (setprod K1 K2)) (λq : set ⇒ (((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)) (a,b) Hab).
Apply andI to the current goal.
We prove the intermediate claim Ha0: ((a,b) 0) 0 = (a 0).
rewrite the current goal using (tuple_2_0_eq a b) (from left to right).
Use reflexivity.
We prove the intermediate claim Hb0: ((a,b) 1) 0 = (b 0).
rewrite the current goal using (tuple_2_1_eq a b) (from left to right).
Use reflexivity.
rewrite the current goal using Ha0 (from right to left).
rewrite the current goal using Hb0 (from right to left).
An exact proof term for the current goal is (andEL ((((a,b) 0) 0,((a,b) 1) 0) ∈ le1) ((((a,b) 0) 1,((a,b) 1) 1) ∈ le2) Hraw).
We prove the intermediate claim Ha1: ((a,b) 0) 1 = (a 1).
rewrite the current goal using (tuple_2_0_eq a b) (from left to right).
Use reflexivity.
We prove the intermediate claim Hb1: ((a,b) 1) 1 = (b 1).
rewrite the current goal using (tuple_2_1_eq a b) (from left to right).
Use reflexivity.
rewrite the current goal using Ha1 (from right to left).
rewrite the current goal using Hb1 (from right to left).
An exact proof term for the current goal is (andER ((((a,b) 0) 0,((a,b) 1) 0) ∈ le1) ((((a,b) 0) 1,((a,b) 1) 1) ∈ le2) Hraw).
∎