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.
Let x3 of type ιο be given.
Let x4 of type ιο be given.
Let x5 of type ιο be given.
Assume H0: ∀ x6 . ∀ x7 x8 : ι → ι → ο . ∀ x9 x10 : ι → ο . x5 (pack_r_r_p_p x6 x7 x8 x9 x10).
The subproof is completed by applying H0 with x0, x1, x2, x3, x4.