Proofgold Proposition

∀ x0 x1 x2 . ∀ x3 x4 : ι → ι . inj x0 x1 x3 ⟶ inj x1 x2 x4 ⟶ inj x0 x2 (λ x5 . x4 (x3 x5))

type
prop

theory
HotG

name
inj_comp

proof
PUfcG..

Megalodon
inj_comp

proofgold address
TMRsf..^inj_comp

creator
14561 Pr4zB../0ae72..

owner
14561 Pr4zB../0ae72..

term root
649bd..