Step * of Lemma shorten-tuple-simplify

[p:Top × Top × Top]. (fst(shorten-tuple(p;1)) fst(snd(p)))
BY
((D THENA Auto) THEN RepeatFor (D -1) THEN Reduce THEN Auto) }


Latex:


Latex:
\mforall{}[p:Top  \mtimes{}  Top  \mtimes{}  Top].  (fst(shorten-tuple(p;1))  \msim{}  fst(snd(p)))


By


Latex:
((D  0  THENA  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  Reduce  0  THEN  Auto)




Home Index