Let α and β be given.
Assume H1: α ⊆ β.
Let x be given.
Assume H2: x ∈ α ∪ {γ '|γ ∈ α}.
Apply binunionE α {γ '|γ ∈ α} x H2 to the current goal.
Assume H3: x ∈ α.
We will prove x ∈ β ∪ {γ '|γ ∈ β}.
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 ∈ {γ '|γ ∈ α}.
We will prove x ∈ β ∪ {γ '|γ ∈ β}.
Apply binunionI2 to the current goal.
We will prove x ∈ {γ '|γ ∈ β}.
Apply ReplE_impred α (λγ ⇒ γ ') x H3 to the current goal.
Let γ be given.
Assume H4: γ ∈ α.
Assume H5: x = γ '.
rewrite the current goal using H5 (from left to right).
We will prove γ ' ∈ {γ '|γ ∈ β}.
An exact proof term for the current goal is ReplI β (λγ ⇒ γ ') γ (H1 γ H4).
∎