---

Step * of Lemma atom_eq_sq_normalize

∀[b1,b2,i,j:Top].  (if i=j then b1[i] else b2 fi  ~ if i=j then b1[j] else b2 fi )
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``so_apply`` 0
   THEN SqEqualBase
   THEN SqequalSqle
   THEN AssumeHasValue
   THEN (HasValueD (-1) ORELSE (ExceptionCases (-1) THEN Try (SameException)))
   THEN Try (((Decide ⌜i = j ∈ Atom⌝⋅ THENA Trivial)
              THEN Try ((HypSubst' (-1) 0 THEN Auto))
              THEN (Assert b2 ≤ b2 BY
                          Auto)
              THEN NthHypSq (-1)
              THEN EqCD
              THEN Refine `atom_eqReduceFalseSq` []
              THEN Auto))) }

1
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 ∈ Atom
7. is-exception(j)
⊢ if i=j then b1 i else b2 fi  ≤ if i=j then b1 j else b2 fi 

2
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 

---

Latex:

---

Latex:
\mforall{}[b1,b2,i,j:Top].    (if  i=j  then  b1[i]  else  b2  fi    \msim{}  if  i=j  then  b1[j]  else  b2  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``so\_apply``  0
  THEN  SqEqualBase
  THEN  SqequalSqle
  THEN  AssumeHasValue
  THEN  (HasValueD  (-1)  ORELSE  (ExceptionCases  (-1)  THEN  Try  (SameException)))
  THEN  Try  (((Decide  \mkleeneopen{}i  =  j\mkleeneclose{}\mcdot{}  THENA  Trivial)
                        THEN  Try  ((HypSubst'  (-1)  0  THEN  Auto))
                        THEN  (Assert  b2  \mleq{}  b2  BY
                                                Auto)
                        THEN  NthHypSq  (-1)
                        THEN  EqCD
                        THEN  Refine  `atom\_eqReduceFalseSq`  []
                        THEN  Auto)))

---

Home Index