theorem instIndependentContinuantAtToParent
theorem instIndependentContinuantAtToParent
: ∀ (x t : Type) [IndependentContinuant.At x t], Continuant.At x t