theorem instCoeDepTypeMaterialEntityOfIs._proof_1
theorem instCoeDepTypeMaterialEntityOfIs._proof_1: ∀ (x : Type) [ta3nj1a4.MaterialEntity.Is x], ta3nj1a4.MaterialEntity.Is x
theorem instCoeDepTypeMaterialEntityOfIs._proof_1
theorem instCoeDepTypeMaterialEntityOfIs._proof_1: ∀ (x : Type) [ta3nj1a4.MaterialEntity.Is x], ta3nj1a4.MaterialEntity.Is x