Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ι . ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . tuple_p (x1 x3) x4 ⟶ ∀ x5 : ι → ι . (∀ x6 . x6 ∈ x1 x3 ⟶ c40a3.. x0 x1 x2 (ap x4 x6) (x5 x6)) ⟶ c40a3.. x0 x1 x2 (lam 2 (λ x6 . If_i (x6 = 0) x3 x4)) (x2 x3 x4 (lam (x1 x3) x5))

type
prop

theory
HotG

name
-

proof
PUbKm..

Megalodon
-

proofgold address
TMTbw..

creator
11610 PrGxv../92659..

owner
11610 PrGxv../92659..

term root
412f1..