Let x0 of type ι be given.
Apply H0 with
λ x1 . x1 = 2c81e.. (f482f.. x1 4a7ef..) (decode_p (f482f.. x1 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))).
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Apply unknownprop_5a3da60961dc828c3b054c11b04e3fdd5c1744838c2dc7756fea2affd3e32f1d with
x1,
x2,
x3,
λ x4 x5 . 2c81e.. x1 x2 x3 = 2c81e.. x4 (decode_p (f482f.. (2c81e.. x1 x2 x3) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (2c81e.. x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..)))).
Apply unknownprop_7159eabc70193e3e4a0586b87e291d6e8bd4060313d3e9dc9d23219e8dc31dc2 with
x1,
x2,
decode_p (f482f.. (2c81e.. x1 x2 x3) (4ae4a.. 4a7ef..)),
x3,
decode_p (f482f.. (2c81e.. x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.
Let x4 of type ι be given.
Apply unknownprop_f89b2eb83b1375e36cd0ad303ce6605f299e4461f16d1e3558e0856c6ba04a59 with
x1,
x2,
x3,
x4,
λ x5 x6 : ο . iff (x2 x4) x5 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying iff_refl with x2 x4.
Let x4 of type ι be given.
Apply unknownprop_353e1ebd952cdfa03484f2eb926c90f10068fbb8a5e3cf11a3a5f72589e7c77c with
x1,
x2,
x3,
x4,
λ x5 x6 : ο . iff (x3 x4) x5 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying iff_refl with x3 x4.