Let x0 of type ο be given.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
x0,
not x0.
The subproof is completed by applying unknownprop_067bff8a3006a4231cc58926bfd8fa619cc0d4504a431e24a5ead7694d33e321 with x0.