Step * 1 of Lemma atom_eq_sq_normalize


1. b2 Base
2. b1 Base
3. Base
4. Base
5. is-exception(if i=j then b1 else b2 fi )
6. i ∈ Atom
7. is-exception(j)
⊢ if i=j then b1 else b2 fi  ≤ if i=j then b1 else b2 fi 
BY
(ExceptionSqequal (-1) THEN HypSubst' (-1) THEN RW (SweepDnC AtomEqExceptionC) THEN Auto) }


Latex:


Latex:

1.  b2  :  Base
2.  b1  :  Base
3.  j  :  Base
4.  i  :  Base
5.  is-exception(if  i=j  then  b1  i  else  b2  fi  )
6.  i  \mmember{}  Atom
7.  is-exception(j)
\mvdash{}  if  i=j  then  b1  i  else  b2  fi    \mleq{}  if  i=j  then  b1  j  else  b2  fi 


By


Latex:
(ExceptionSqequal  (-1)  THEN  HypSubst'  (-1)  0  THEN  RW  (SweepDnC  AtomEqExceptionC)  0  THEN  Auto)




Home Index