Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2: x0 = x1 ⟶ ∀ x2 : ο . x2.
Apply unknownprop_350f82fd4df83c2030aa9fe95c59b3e2660a97bcb0cb01e460d56aaef04b44cb with
4ae4a.. (4ae4a.. 4a7ef..),
λ x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) x2 leaving 3 subgoals.
The subproof is completed by applying unknownprop_db15d8db2f5eec557f7b3f5a742d4a0a45fde052cadd58f24d03c6c32a463f49.
Let x2 of type ι be given.
Apply unknownprop_285d1412c16abfd3320f0ee89e600fad3199271183754290c3d7bd1f86d5a491 with
x2,
λ x3 . prim1 (f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x0 x1)) x3) (4ae4a.. (4ae4a.. 4a7ef..)) leaving 3 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_67d8fddea88125b50903f4bd482ed1753cb719c67016df79894ab3055421315b with
x0,
x1,
λ x3 x4 . prim1 x4 (4ae4a.. (4ae4a.. 4a7ef..)).
The subproof is completed by applying H0.
Apply unknownprop_327f4faff65d2b4b341be7a5ceca39a573a558eea38825726ce72538879f3bc4 with
x0,
x1,
λ x3 x4 . prim1 x4 (4ae4a.. (4ae4a.. 4a7ef..)).
The subproof is completed by applying H1.
Let x2 of type ι be given.
Let x3 of type ι be given.