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