Step
*
of Lemma
record+_subtype_rel
∀[T:Type]. ∀[B:T ⟶ Type]. ∀[z:Atom].  (T; z:B[self] ⊆r T)
BY
{ Auto }
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[B:T  {}\mrightarrow{}  Type].  \mforall{}[z:Atom].    (T;  z:B[self]  \msubseteq{}r  T)
By
Latex:
Auto
Home
Index