Step
*
of Lemma
append-empty-nat-seq
∀[f:finite-nat-seq()]. ∀[g:Top]. (f**g^(0) = f ∈ finite-nat-seq())
BY
{ ((UnivCD THENA Auto)
THEN RepUR ``append-finite-nat-seq`` 0
THEN D 1
THEN Reduce 0
THEN RepUR ``finite-nat-seq mk-finite-nat-seq`` 0
THEN (Subst ⌜n + 0 ~ n⌝ 0⋅ THENA Auto)
THEN EqCD
THEN Auto) }
Latex:
Latex:
\mforall{}[f:finite-nat-seq()]. \mforall{}[g:Top]. (f**g\^{}(0) = f)
By
Latex:
((UnivCD THENA Auto)
THEN RepUR ``append-finite-nat-seq`` 0
THEN D 1
THEN Reduce 0
THEN RepUR ``finite-nat-seq mk-finite-nat-seq`` 0
THEN (Subst \mkleeneopen{}n + 0 \msim{} n\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN EqCD
THEN Auto)
Home
Index