---

Step * 1 of Lemma rv-nontrivial


1. n : {2...}
⊢ λi.r0 ≠ λi.if (i =z 0) then r1 else r0 fi 
BY
{ (RepUR ``real-vec-sep`` 0
   THEN (Assert ⌜d(λi.r0;λi.if (i =z 0) then r1 else r0 fi ) = r1⌝⋅ THENM (RWO  "-1" 0 THEN Auto))
   ) }

1
.....assertion..... 
1. n : {2...}
⊢ d(λi.r0;λi.if (i =z 0) then r1 else r0 fi ) = r1

---

Latex:

---

Latex:

1.  n  :  \{2...\}
\mvdash{}  \mlambda{}i.r0  \mneq{}  \mlambda{}i.if  (i  =\msubz{}  0)  then  r1  else  r0  fi 


By

---

Latex:
(RepUR  ``real-vec-sep``  0
  THEN  (Assert  \mkleeneopen{}d(\mlambda{}i.r0;\mlambda{}i.if  (i  =\msubz{}  0)  then  r1  else  r0  fi  )  =  r1\mkleeneclose{}\mcdot{}  THENM  (RWO    "-1"  0  THEN  Auto))
  )

---

Home Index