| pf |
|---|
Let x0 of type ι be given.
Apply H0 with λ x1 . x1 = 38265.. (f482f.. x1 4a7ef..) (decode_c (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (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_9ab42cc1d9ed743f0be0840608d015cffc14cffaf27bca7b726dbccfb1bdf67c with x1, x2, x3, x4, x5, λ x6 x7 . 38265.. x1 x2 x3 x4 x5 = 38265.. x6 (decode_c (f482f.. (38265.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (38265.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (38265.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. (38265.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_56e2b9fcf151cd7985b2f5a71445df33f8c38d2de58395ef3f0b8a2c9f8cb01e with x1, x2, decode_c (f482f.. (38265.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (38265.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, 2b2e3.. (f482f.. (38265.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, 2b2e3.. (f482f.. (38265.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
Let x6 of type ι → ο be given.
Assume H2: ∀ x7 . x6 x7 ⟶ prim1 x7 x1. Apply unknownprop_011ac084cf6e5416328fa6ff3d522814add523228b1ff93a734d85483d30b1fe with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x2 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x2 x6.
The subproof is completed by applying unknownprop_81a9574ea54c5e428379e6db95c9ef2560ddef7ab293597b07f3639d68bec0b7 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_f625f431cb41827fe9d3f8717ebcd1125ff7d57e80c33b9ff8170810d3ee3ff1 with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x4 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying iff_refl with x4 x6 x7.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_74d95a80feb61e497681f176afc3b59335043706622d96810e7337299988a1ce with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x5 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying iff_refl with x5 x6 x7.
■ |
|