---

Step * of Lemma manames-overlap-nil

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

---

Latex:


\mforall{}[x,y:Top].  \mforall{}[nms:MaName  List].    (if  []  and  nms  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