`BookProof.HalfLineLimitCircle.hlKin_apply` (f : testSpace) : hlKin (hlEquiv f) = -testIncl (deriv2LM f)

Initializing...

`BookProof.HalfLineLimitCircle.hlKin_apply` (f : testSpace) : hlKin (hlEquiv f) = -testIncl (deriv2LM f) · Prove2Me