Step
*
of Lemma
fpf-null-domain
∀[A:Type]. ∀[B:A ─→ Type]. ∀[f:Void ─→ Top]. (<[], f> = ⊗ ∈ x:A fp-> B[x])
BY
{ (Auto
THEN Unfolds ``fpf fpf-empty`` 0
THEN EqCD
THEN Auto
THEN ExtWith [`z'] [⌈Void ─→ Top⌉]⋅
THEN Reduce 0
THEN Auto
THEN D (-2)
THEN Auto
THEN FLemma `nil_member` [-2]
THEN Auto) }
Latex:
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[f:Void {}\mrightarrow{} Top]. (<[], f> = \motimes{})
By
(Auto
THEN Unfolds ``fpf fpf-empty`` 0
THEN EqCD
THEN Auto
THEN ExtWith [`z'] [\mkleeneopen{}Void {}\mrightarrow{} Top\mkleeneclose{}]\mcdot{}
THEN Reduce 0
THEN Auto
THEN D (-2)
THEN Auto
THEN FLemma `nil\_member` [-2]
THEN Auto)
Home
Index