Let X, Y, eX, eY and f be given.
Set Phi to be the term
λX eX Y eY ⇒ f ∈ YX ∧ f eX = eY of type
set → set → set → set → prop.
Set PhiX to be the term λX eX ⇒ unpack_e_o (pack_e Y eY) (λY' eY ⇒ Phi X eX Y' eY) of type set → set → prop.
We will prove unpack_e_o (pack_e X eX) PhiX = Phi X eX Y eY.
Use transitivity with and PhiX X eX.
An exact proof term for the current goal is unpack_e_o_eq PhiX X eX.
We will prove unpack_e_o (pack_e Y eY) (Phi X eX) = Phi X eX Y eY.
An exact proof term for the current goal is unpack_e_o_eq (Phi X eX) Y eY.