Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_27feba477a8f3841ddc6f3e3e4133988fc5187f1062e005dcb0fbdade0dcf4a5 with
x0,
x1,
λ x3 x4 . prim1 x3 (b5c9f.. x2 (4ae4a.. (4ae4a.. 4a7ef..))).
Apply unknownprop_78f4273a7b4d13f02d77d194b65be481121674fd021f4ffb88d69be4bcd0ab71 with
4ae4a.. (4ae4a.. 4a7ef..),
λ x3 . x2,
λ x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x0 x1)) x3.
Let x3 of type ι be given.
Apply unknownprop_285d1412c16abfd3320f0ee89e600fad3199271183754290c3d7bd1f86d5a491 with
x3,
λ x4 . prim1 (f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x5 . If_i (x5 = 4a7ef..) x0 x1)) x4) x2 leaving 3 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_67d8fddea88125b50903f4bd482ed1753cb719c67016df79894ab3055421315b with
x0,
x1,
λ x4 x5 . prim1 x5 x2.
The subproof is completed by applying H0.
Apply unknownprop_327f4faff65d2b4b341be7a5ceca39a573a558eea38825726ce72538879f3bc4 with
x0,
x1,
λ x4 x5 . prim1 x5 x2.
The subproof is completed by applying H1.