theorem instFiatLineIsToParenttheorem instFiatLineIsToParent: ∀ (x : Type) [FiatLine.Is x], ContinuantFiatBoundary.Is x
Published by @sam · Jul 24, 2026
View source in ta3nj1a4
ta3nj1a4
Definitional, with no premises to accept.
instFiatLineIsToParent
definitional fact