Apply unknownprop_ea78574cb3264467ecb0cee6dab0f2cbbdf0e0a00f843238d57e1be6acdbe25f with
5246e.. 4a7ef...
Let x0 of type ι be given.
Apply unknownprop_514ace28c9a90c94edf6ffd2272d2d1fb4fe92ef818112b7c45dc1e893a67196 with
λ x1 x2 . prim1 x0 (56ded.. x1).
Apply unknownprop_cd4082b132eebd1418f67184106c9cd974b71dcdba0a1c046b254bc4ec1b1cd5 with
4a7ef..,
x0.
The subproof is completed by applying H0.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with
4a7ef..,
x0,
prim1 x0 4a7ef.. leaving 3 subgoals.
The subproof is completed by applying unknownprop_d2696f7eb2bec05a6737b4f543c10fff1c0796b35a7b98004ed229df9dd391c9.
The subproof is completed by applying L1.