Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι be given.
Assume H0: inj (e5b72.. 48ef8..) 48ef8.. x0.
Apply H0 with False.
Assume H1: ∀ x1 . prim1 x1 (e5b72.. 48ef8..) ⟶ prim1 (x0 x1) 48ef8...
Assume H2: ∀ x1 . prim1 x1 (e5b72.. 48ef8..) ⟶ ∀ x2 . prim1 x2 (e5b72.. 48ef8..) ⟶ x0 x1 = x0 x2 ⟶ x1 = x2.
Claim L3: prim1 (a4c2a.. (e5b72.. 48ef8..) (λ x1 . nIn (x0 x1) x1) (λ x1 . x0 x1)) (e5b72.. 48ef8..)
Apply unknownprop_85c22e88a806aabda7246f27ac458442bcb94ac25cc9a3616a68cf646d95941d with 48ef8.., a4c2a.. (e5b72.. 48ef8..) (λ x1 . nIn (x0 x1) x1) (λ x1 . x0 x1).
Let x1 of type ι be given.
Assume H3: prim1 x1 (a4c2a.. (e5b72.. 48ef8..) (λ x2 . nIn (x0 x2) x2) (λ x2 . x0 x2)).
Apply unknownprop_e546e9a8cc28c7314a8604ada98e2a83641f2ef6b8078441570ffe037b28d26f with e5b72.. 48ef8.., λ x2 . nIn (x0 x2) x2, x0, x1, prim1 x1 48ef8.. leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: prim1 x2 (e5b72.. 48ef8..).
Assume H5: nIn (x0 x2) x2.
Assume H6: x1 = x0 x2.
Apply H6 with λ x3 x4 . prim1 x4 48ef8...
Apply H1 with ....
...
Claim L4: nIn (x0 (a4c2a.. (e5b72.. 48ef8..) (λ x1 . nIn (x0 x1) x1) (λ x1 . x0 x1))) (a4c2a.. (e5b72.. 48ef8..) (λ x1 . nIn (x0 x1) x1) (λ x1 . x0 x1))
Assume H4: prim1 (x0 (a4c2a.. (e5b72.. 48ef8..) (λ x1 . nIn (x0 x1) x1) (λ x1 . x0 x1))) (a4c2a.. (e5b72.. 48ef8..) (λ x1 . nIn (x0 x1) x1) (λ x1 . x0 x1)).
Apply unknownprop_e546e9a8cc28c7314a8604ada98e2a83641f2ef6b8078441570ffe037b28d26f with e5b72.. 48ef8.., λ x1 . nIn (x0 x1) x1, x0, x0 (a4c2a.. (e5b72.. 48ef8..) (λ x1 . nIn (x0 x1) x1) (λ x1 . x0 x1)), False leaving 2 subgoals.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H5: prim1 x1 (e5b72.. 48ef8..).
Assume H6: nIn (x0 x1) x1.
Assume H7: x0 (a4c2a.. (e5b72.. 48ef8..) (λ x2 . nIn (x0 x2) x2) (λ x2 . x0 x2)) = x0 x1.
Claim L8: a4c2a.. (e5b72.. 48ef8..) (λ x2 . nIn (x0 x2) x2) (λ x2 . x0 x2) = x1
Apply H2 with a4c2a.. (e5b72.. 48ef8..) (λ x2 . nIn (x0 x2) x2) (λ x2 . x0 x2), x1 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H5.
The subproof is completed by applying H7.
Apply H6.
Apply L8 with λ x2 x3 . prim1 (x0 x2) x2.
The subproof is completed by applying H4.
Apply L4.
Apply unknownprop_9c424e90871cd9e3a05e6a3be208792c52ad17517e2db8ef40187e46ac0e9a6e with e5b72.. 48ef8.., λ x1 . nIn (x0 x1) x1, x0, a4c2a.. (e5b72.. 48ef8..) (λ x1 . nIn (x0 x1) x1) (λ x1 . x0 x1) leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
■