Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0x1 x3 = x2 x3)94f9e.. (1ad11.. x0 (91630.. 4a7ef..)) (λ x3 . x1 x3) = 94f9e.. (1ad11.. x0 (91630.. 4a7ef..)) (λ x3 . x2 x3)
Let x0 of type ι be given.
Let x1 of type ιι be given.
Let x2 of type ιι be given.
Assume H0: ∀ x3 . prim1 x3 x0x1 x3 = x2 x3.
Apply unknownprop_59be5eee144fb0f12156456c7f9888c3f0525fea126d0d8cdf71e5c53005d86a with 1ad11.. x0 (91630.. 4a7ef..), x1, x2.
Let x3 of type ι be given.
Assume H1: prim1 x3 (1ad11.. x0 (91630.. 4a7ef..)).
Apply H0 with x3.
Apply unknownprop_f3a4771d3d9a8514b2ad16b328a764b0ce93421ae4df5a6923d3e167d035e33a with x0, 91630.. 4a7ef.., x3.
The subproof is completed by applying H1.
Apply In_rec_i_eq with λ x0 . λ x1 : ι → ι . 94f9e.. (1ad11.. x0 (91630.. 4a7ef..)) (λ x2 . x1 x2).
The subproof is completed by applying L0.