- â\88\80t,p. t ϵ ð\9d\90\83ð\9d\9b\97 → p ϵ t →
- ∨∨ ∃∃n. #n ⇔ t & 𝗱❨n❩;𝐞 = p
- | â\88\83â\88\83u,q,n. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & ð\9d\9b\97n.u â\87\94 t & ð\9d\97±â\9d¨nâ\9d©;q = p
- | â\88\83â\88\83u,q. u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & ð\9d\9b\8c.u â\87\94 t & ð\9d\97\9f;q = p
- | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ u & @v.u â\87\94 t & ð\9d\97\94;q = p
- | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\97 & u ϵ ð\9d\90\83ð\9d\9b\97 & q ϵ v & @v.u â\87\94 t & ð\9d\97¦;q = p
+ â\88\80t,p. t ϵ ð\9d\90\83ð\9d\9b\95 → p ϵ t →
+ ∨∨ ∃∃n. #n ⇔ t & 𝗱n◗𝐞 = p
+ | â\88\83â\88\83u,q,n. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & ð\9d\9b\95n.u â\87\94 t & ð\9d\97±nâ\97\97ð\9d\97ºâ\97\97q = p
+ | â\88\83â\88\83u,q. u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & ð\9d\9b\8c.u â\87\94 t & ð\9d\97\9fâ\97\97q = p
+ | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ u & @v.u â\87\94 t & ð\9d\97\94â\97\97q = p
+ | â\88\83â\88\83v,u,q. v ϵ ð\9d\90\83ð\9d\9b\95 & u ϵ ð\9d\90\83ð\9d\9b\95 & q ϵ v & @v.u â\87\94 t & ð\9d\97¦â\97\97q = p