Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
λ x2 . struct_p (20e9b.. x2 x1).
Let x2 of type ι be given.
Let x3 of type ι → ο be given.
Apply H1 with
λ x4 . struct_p (20e9b.. (pack_p x2 x3) x4).
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Apply unknownprop_b136686cda57813ec105d14134466864c52e8c5ca85ea4790197540126814cf6 with
x2,
x3,
x4,
x5,
λ x6 x7 . struct_p x7.