Proofgold Object

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

type
ι → (ι → ι) → ι → ο

theory
HotG

name
-

definition
PUbKm..

Megalodon
-

proofgold address
TMaL1..

creator
11610 PrGxv../38191..

owner
11610 PrGxv../38191..

term root
2cc59..