Let le, K, a and b be given.

Assume Hab: (a,b) ∈ le.

Assume HaK: a ∈ K.

Assume HbK: b ∈ K.

We will prove (a,b) ∈ rel_restrict le K.

rewrite the current goal using (rel_restrict_def le K) (from left to right).

Apply (SepI le (λp : set ⇒ p 0 ∈ K ∧ p 1 ∈ K) (a,b) Hab) to the current goal.

Apply andI to the current goal.

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

An exact proof term for the current goal is HaK.

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

An exact proof term for the current goal is HbK.

∎