Let alpha and beta be given.
Assume H1: alpha ⊆ beta.
Let x be given.
Assume H2: x ∈ alpha ∪ {gamma '|gamma ∈ alpha}.
Apply binunionE alpha {gamma '|gamma ∈ alpha} x H2 to the current goal.
Assume H3: x ∈ alpha.
We will prove x ∈ beta ∪ {gamma '|gamma ∈ beta}.
Apply binunionI1 to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is H3.
Assume H3: x ∈ {gamma '|gamma ∈ alpha}.
We will prove x ∈ beta ∪ {gamma '|gamma ∈ beta}.
Apply binunionI2 to the current goal.
We will prove x ∈ {gamma '|gamma ∈ beta}.
Apply ReplE_impred alpha (λgamma ⇒ gamma ') x H3 to the current goal.
Let gamma be given.
Assume H4: gamma ∈ alpha.
Assume H5: x = gamma '.
rewrite the current goal using H5 (from left to right).
We will prove gamma ' ∈ {gamma '|gamma ∈ beta}.
An exact proof term for the current goal is ReplI beta (λgamma ⇒ gamma ') gamma (H1 gamma H4).
∎