Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2 ⟶ ∀ x3 . nat_p x3 ⟶ and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 1)

as obj
-

as prop
75cbc..^{SNo_sqrtaux_mon_lem}

theory
HotG

stx
87341..

address
TMdT3..^{SNo_sqrtaux_mon_lem}