Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = 6640c.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Let x4 of type ι → ι be given.
Let x5 of type ι be given.
Apply unknownprop_991b7de395beb4512722a3149132d9dce8cb5d28abc1d7618825d7b6d5e0ae73 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . 6640c.. x1 x2 x3 x4 x5 = 6640c.. x6 (e3162.. (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_332b8379ba1b9430b61df86c7f3eb35c9d7e7de536d248b3115455b6211390d4 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . 6640c.. x1 x2 x3 x4 x5 = 6640c.. x1 (e3162.. (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6.
Apply unknownprop_7a35e90ac4e848f32f97fe9b3dd300994f7d820208333a551f44b924f4cc91ca with
x1,
x2,
e3162.. (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
x3,
e3162.. (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))),
x4,
f482f.. (f482f.. (6640c.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))),
x5 leaving 3 subgoals.
The subproof is completed by applying unknownprop_a25716e8b518a69d0f9d585cf94f6f04c7c0704c47c4c1ad085671f36c1228f7 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_296e229c05a4e616c28cc0a5443f002c701ae842cf0a7b85ac73926ff7fade43 with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_d7fd60967948dce86022f00e57252b30ac620098238bb49861e08fc81f8bbcd9 with x1, x2, x3, x4, x5.