---

Step * 1 of Lemma aa_max_w_unit_prop1


1. i : @i
2. wu : ?@i
 j:. (case wu of inl(intval2) => inl imax(i;intval2)  | inr(unitval2) => inl i  = (inl j ))
BY
{ DVar `wu' THEN Reduce 0 THEN MaAuto }

1
1. i : @i
2. x : @i
 j:. ((inl imax(i;x) ) = (inl j ))



1.  i  :  \mBbbZ{}@i
2.  wu  :  \mBbbZ{}?@i
\mvdash{}  \mexists{}j:\mBbbZ{}.  (case  wu  of  inl(intval2)  =>  inl  imax(i;intval2)    |  inr(unitval2)  =>  inl  i    =  (inl  j  ))


By

DVar  `wu'  THEN  Reduce  0  THEN  MaAuto



Home Index