---

Step * of Lemma manames-overlap-case-symmetry

∀[x,y:Top]. ∀[nms1,nms2:MaName List].
  (if nms1 and nms2 overlap then x else y fi ~ if nms2 and nms1 overlap then x else y fi)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `manames-overlap-case` 0
   THEN RepeatFor 2 (Branch 0)
   THEN OnMaybeHyp 7 (\h. (D h THEN BLemma `l_disjoint-symmetry` THEN Complete (Auto)))) }

---

Latex:


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


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `manames-overlap-case`  0
  THEN  RepeatFor  2  (Branch  0)
  THEN  OnMaybeHyp  7  (\mbackslash{}h.  (D  h  THEN  BLemma  `l\_disjoint-symmetry`  THEN  Complete  (Auto))))

---

Home Index