Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Assume H0:
In x2 (Repl x0 x1).
Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with
λ x3 . In x3 x0,
λ x3 . x2 = x1 x3.
Apply unknownprop_74e6ddb76e51f556d0e4a910f649c4782bc9cb375d38baef38a8c05a47e8ef22 with
x0,
x1,
x2.
The subproof is completed by applying H0.