Let le, K, a and b be given.
We prove the intermediate
claim HabK':
(a,b) ∈ {p ∈ le|p 0 ∈ K ∧ p 1 ∈ K}.
An exact proof term for the current goal is HabK.
We prove the intermediate
claim Hraw:
(a,b) ∈ le ∧ ((a,b) 0 ∈ K ∧ (a,b) 1 ∈ K).
An
exact proof term for the current goal is
(SepE le (λp : set ⇒ p 0 ∈ K ∧ p 1 ∈ K) (a,b) HabK').
We prove the intermediate
claim Hab:
(a,b) ∈ le.
An
exact proof term for the current goal is
(andEL ((a,b) ∈ le) (((a,b) 0 ∈ K ∧ (a,b) 1 ∈ K)) Hraw).
We prove the intermediate
claim Ha0:
((a,b) 0) ∈ K.
An
exact proof term for the current goal is
(andEL (((a,b) 0 ∈ K)) (((a,b) 1 ∈ K)) (andER ((a,b) ∈ le) (((a,b) 0 ∈ K ∧ (a,b) 1 ∈ K)) Hraw)).
We prove the intermediate
claim Hb1:
((a,b) 1) ∈ K.
An
exact proof term for the current goal is
(andER (((a,b) 0 ∈ K)) (((a,b) 1 ∈ K)) (andER ((a,b) ∈ le) (((a,b) 0 ∈ K ∧ (a,b) 1 ∈ K)) Hraw)).
Apply and3I to the current goal.
An exact proof term for the current goal is Hab.
rewrite the current goal using
(tuple_2_0_eq a b) (from right to left).
An exact proof term for the current goal is Ha0.
rewrite the current goal using
(tuple_2_1_eq a b) (from right to left).
An exact proof term for the current goal is Hb1.