Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι be given.
Assume H0: surj 48ef8.. (e5b72.. 48ef8..) x0.
Apply H0 with False.
Assume H1: ∀ x1 . prim1 x1 48ef8.. ⟶ prim1 (x0 x1) (e5b72.. 48ef8..).
Assume H2: ∀ x1 . prim1 x1 (e5b72.. 48ef8..) ⟶ ∃ x2 . and (prim1 x2 48ef8..) (x0 x2 = x1).
Claim L3: prim1 (1216a.. 48ef8.. (λ x1 . nIn x1 (x0 x1))) (e5b72.. 48ef8..)
Apply unknownprop_85c22e88a806aabda7246f27ac458442bcb94ac25cc9a3616a68cf646d95941d with 48ef8.., 1216a.. 48ef8.. (λ x1 . nIn x1 (x0 x1)).
Let x1 of type ι be given.
Assume H3: prim1 x1 (1216a.. 48ef8.. (λ x2 . nIn x2 (x0 x2))).
Apply unknownprop_78dd4d18930f8cdb1d353eca6deb6db797599b58a01b747c9a28b7030299025c with 48ef8.., λ x2 . nIn x2 (x0 x2), x1.
The subproof is completed by applying H3.
Apply H2 with 1216a.. 48ef8.. (λ x1 . nIn x1 (x0 x1)), False leaving 2 subgoals.
The subproof is completed by applying L3.
Let x1 of type ι be given.
Assume H4: (λ x2 . and (prim1 x2 48ef8..) (x0 x2 = 1216a.. 48ef8.. (λ x3 . nIn x3 (x0 x3)))) x1.
Apply H4 with False.
Assume H5: prim1 x1 48ef8...
Assume H6: x0 x1 = 1216a.. 48ef8.. (λ x2 . nIn x2 (x0 x2)).
Claim L7: nIn x1 (1216a.. 48ef8.. (λ x2 . nIn x2 (x0 x2)))
Assume H7: prim1 x1 (1216a.. 48ef8.. (λ x2 . nIn x2 (x0 x2))).
Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with 48ef8.., λ x2 . nIn x2 (x0 x2), x1 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply H6 with λ x2 x3 . prim1 x1 x3.
The subproof is completed by applying H7.
Apply L7.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with 48ef8.., λ x2 . nIn x2 (x0 x2), x1 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply H6 with λ x2 x3 . nIn x1 x3.
The subproof is completed by applying L7.
■