Let X and y be given.
Assume HX H1.
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Apply and3I to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is H1a.
Let z be given.
Let x be given.
rewrite the current goal using Hze (from left to right).
An exact proof term for the current goal is H1c x Hx (HX x Hx).
∎