Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι → ο . (∀ x3 x4 x5 . x0 x3x0 x4x2 x3 x4 x5x5setexp (x1 x4) (x1 x3))(∀ x3 . x0 x3x2 x3 x3 (lam_id (x1 x3)))(∀ x3 x4 x5 x6 x7 . x0 x3x0 x4x0 x5x2 x3 x4 x6x2 x4 x5 x7x2 x3 x5 (lam_comp (x1 x3) x7 x6))MetaFunctor_strict x0 x2 (λ x3 . lam_id (x1 x3)) (λ x3 x4 x5 . lam_comp (x1 x3)) (λ x3 . True) HomSet lam_id (λ x3 x4 x5 . lam_comp x3) x1 (λ x3 x4 x5 . x5)
as obj
-
as prop
ec1a3..MetaCatConcreteForgetful_strict
theory
HotG
stx
820be..
address
TMLMT..MetaCatConcreteForgetful_strict