Proofgold Proposition

∀ x0 x1 x2 x3 . x0 ∈ 4 ⟶ x1 ∈ 4 ⟶ x2 ∈ 4 ⟶ x3 ∈ 4 ⟶ (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ bij 4 4 (ap (lam 4 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 (If_i (x4 = 2) x2 x3)))))

type
prop

theory
HotG

name
tuple_4_bij_4

proof
PUPjJ..

Megalodon
tuple_4_bij_4

proofgold address
TMdGB..^{tuple_4_bij_4}

creator
4909 Pr6Pc../a46de..

owner
4909 Pr6Pc../a46de..

term root
8d7a7..