Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: struct_r x0.
Assume H1: struct_r x1.
Apply H0 with λ x2 . struct_r (3fa3a.. x2 x1).
Let x2 of type ι be given.
Let x3 of type ι → ι → ο be given.
Apply H1 with λ x4 . struct_r (3fa3a.. (pack_r x2 x3) x4).
Let x4 of type ι be given.
Let x5 of type ι → ι → ο be given.
Apply unknownprop_2b21d9fc231c558646c467d14a820e3bc5f0cce785ca7db2a0cb0c92dadc07f5 with x2, x3, x4, x5, λ x6 x7 . struct_r x7.
The subproof is completed by applying pack_struct_r_I with setsum x2 x4, λ x6 x7 . or (and (and (x6 = Inj0 (Unj x6)) (x7 = Inj0 (Unj x7))) (x3 (Unj x6) (Unj x7))) (and (and (x6 = Inj1 (Unj x6)) (x7 = Inj1 (Unj x7))) (x5 (Unj x6) (Unj x7))).
■