Proofgold Term Root Disambiguation

λ x0 . and (Field x0) (∀ x1 . x1 ∈ omega ⟶ nat_primrec (field4 x0) (λ x3 . field1b x0 (field4 x0)) x1 = field3 x0 ⟶ ∀ x2 : ο . x2)

as obj
595d0..

as prop
-

theory
HotG

stx
6b5ba..

address
TMY8z..