Step * of Lemma manames-overlap-nil2

[x,y:Top]. ∀[nms:MaName List].  (if nms and [] overlap then else fi y)
BY
((UnivCD THENA Auto) THEN Unfold `manames-overlap-case` THEN Branch THEN -2 THEN Auto) }


Latex:


\mforall{}[x,y:Top].  \mforall{}[nms:MaName  List].    (if  nms  and  []  overlap  then  x  else  y  fi  \msim{}  y)


By

((UnivCD  THENA  Auto)  THEN  Unfold  `manames-overlap-case`  0  THEN  Branch  0  THEN  D  -2  THEN  Auto)




Home Index