Step
*
of Lemma
product-equipollent-tuple3
∀L:Type List. ∀[A:Type]. tuple-type(L) × A ~ tuple-type(L @ [A])
BY
{ TACTIC:(InductionOnList THEN Reduce 0) }
1
∀[A:Type]. Unit × A ~ A
2
1. u : Type
2. v : Type List
3. ∀[A:Type]. tuple-type(v) × A ~ tuple-type(v @ [A])
⊢ ∀[A:Type]. if null(v) then u else u × tuple-type(v) fi  × A ~ if null(v @ [A]) then u else u × tuple-type(v @ [A]) fi 
Latex:
Latex:
\mforall{}L:Type  List.  \mforall{}[A:Type].  tuple-type(L)  \mtimes{}  A  \msim{}  tuple-type(L  @  [A])
By
Latex:
TACTIC:(InductionOnList  THEN  Reduce  0)
Home
Index