---

Step * 2 of Lemma atom_eq_sq_normalize


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index