==inferring |deref(deref(ptr()))|==
	-{0} deref
	-{1} deref[» [π [Pointer [αti]]] [αti]]
	-{0} deref
	-{1} deref[» [π [Pointer [αzi]]] [αzi]]
	-{0} ptr
	-{1} ptr[» [π] [Pointer [Pointer [Int]]]]
	-{0} ptr[» [π] [Pointer [Pointer [Int]]]]():[αko]
	-{u} [» [π] [αko]]~[» [π] [Pointer [Pointer [Int]]]]
		-{u} [π]~[π]
		-{v} [π]~[π] | cons
		-{u} [αko]~[Pointer [Pointer [Int]]]
		-{v} [Pointer [Pointer [Int]]]~[Pointer [Pointer [Int]]] | lvar
	-{v} [» [π] [Pointer [Pointer [Int]]]]~[» [π] [Pointer [Pointer [Int]]]] | cons
	-{1} ptr[» [π] [Pointer [Pointer [Int]]]]():[Pointer [Pointer [Int]]]
	-{0} deref[» [π [Pointer [αzi]]] [αzi]](ptr[» [π] [Pointer [Pointer [Int]]]]():[Pointer [Pointer [Int]]]):[αno]
	-{u} [» [π [Pointer [Pointer [Int]]]] [αno]]~[» [π [Pointer [αzi]]] [αzi]]
		-{u} [π [Pointer [Pointer [Int]]]]~[π [Pointer [αzi]]]
			-{u} [Pointer [Pointer [Int]]]~[Pointer [αzi]]
				-{u} [Pointer [Int]]~[αzi]
				-{v} [Pointer [Int]]~[Pointer [Int]] | rvar
			-{v} [Pointer [Pointer [Int]]]~[Pointer [Pointer [Int]]] | cons
		-{v} [π [Pointer [Pointer [Int]]]]~[π [Pointer [Pointer [Int]]]] | cons
		-{u} [αno]~[Pointer [Int]]
		-{v} [Pointer [Int]]~[Pointer [Int]] | lvar
	-{v} [» [π [Pointer [Pointer [Int]]]] [Pointer [Int]]]~[» [π [Pointer [Pointer [Int]]]] [Pointer [Int]]] | cons
	-{1} deref[» [π [Pointer [Pointer [Int]]]] [Pointer [Int]]](ptr[» [π] [Pointer [Pointer [Int]]]]():[Pointer [Pointer [Int]]]):[Pointer [Int]]
	-{0} deref[» [π [Pointer [αti]]] [αti]](deref[» [π [Pointer [Pointer [Int]]]] [Pointer [Int]]](ptr[» [π] [Pointer [Pointer [Int]]]]():[Pointer [Pointer [Int]]]):[Pointer [Int]]):[αro]
	-{u} [» [π [Pointer [Int]]] [αro]]~[» [π [Pointer [αti]]] [αti]]
		-{u} [π [Pointer [Int]]]~[π [Pointer [αti]]]
			-{u} [Pointer [Int]]~[Pointer [αti]]
				-{u} [Int]~[αti]
				-{v} [Int]~[Int] | rvar
			-{v} [Pointer [Int]]~[Pointer [Int]] | cons
		-{v} [π [Pointer [Int]]]~[π [Pointer [Int]]] | cons
		-{u} [αro]~[Int]
		-{v} [Int]~[Int] | lvar
	-{v} [» [π [Pointer [Int]]] [Int]]~[» [π [Pointer [Int]]] [Int]] | cons
	-{1} deref[» [π [Pointer [Int]]] [Int]](deref[» [π [Pointer [Pointer [Int]]]] [Pointer [Int]]](ptr[» [π] [Pointer [Pointer [Int]]]]():[Pointer [Pointer [Int]]]):[Pointer [Int]]):[Int]