Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι → ι . 3d151.. (pack_b x0 x1) (pack_b x2 x3) = pack_b (setprod x0 x2) (λ x5 x6 . lam 2 (λ x7 . If_i (x7 = 0) (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1))))

type
prop

theory
HotG

name
-

proof
PUdPp..

Megalodon
-

proofgold address
TMQd2..

creator
11767 PrEBh../4cc72..

owner
11767 PrEBh../4cc72..

term root
84b7a..