Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι(ιιο) → ι be given.
Let x1 of type ι be given.
Let x2 of type ιιο be given.
Assume H0: ∀ x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1∀ x5 . prim1 x5 x1iff (x2 x4 x5) (x3 x4 x5))x0 x1 x3 = x0 x1 x2.
Apply unknownprop_97f8046614ea7148c1fa23ec1426d82a984f022d6441770c46d9508e4193899d with x1, x2, λ x3 x4 . x0 x3 (2b2e3.. (f482f.. (35983.. x1 x2) (4ae4a.. 4a7ef..))) = x0 x1 x2.
Apply H0 with 2b2e3.. (f482f.. (35983.. x1 x2) (4ae4a.. 4a7ef..)).
Let x3 of type ι be given.
Assume H1: prim1 x3 x1.
Let x4 of type ι be given.
Assume H2: prim1 x4 x1.
Apply unknownprop_86d039171608909af3061792cdafdca234dab72c05fe9399d5fd5de804007d06 with x1, x2, x3, x4, λ x5 x6 : ο . iff (x2 x3 x4) x5 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x2 x3 x4.