Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . ∀ x3 : ι → ι . 5a1fb.. (pack_u x0 x1) (pack_u x2 x3) = pack_u (setprod x0 x2) (λ x5 . lam 2 (λ x6 . If_i (x6 = 0) (x1 (ap x5 0)) (x3 (ap x5 1))))

type
prop

theory
HotG

name
-

proof
PUYhi..

Megalodon
-

proofgold address
TMTex..

creator
11768 PrEBh../8abb6..

owner
11768 PrEBh../8abb6..

term root
d4e4b..