theorem BFO.instCoeRealizableEntitySpecificallyDependentContinuant._proof_1
theorem BFO.instCoeRealizableEntitySpecificallyDependentContinuant._proof_1: ∀ (v : hz46pbq2.BFO.RealizableEntity), hz46pbq2.BFO.SpecificallyDependentContinuant.Is (Subtype.val v)