---

Step * of Lemma ifthenelse_sqequal

∀[a,x1,y1,x2,y2:Base].
  if a then x1 else y1 fi  ~ if a then x2 else y2 fi  
  supposing ((∃z:Base. (a ~ inl z)) ⇒ (x1 ~ x2)) ∧ ((∃z:Base. (a ~ inr z )) ⇒ (y1 ~ y2))
BY
{ ((UnivCD THENA Auto)
   THEN D -1
   THEN SqequalSqle
   THEN BLemma `ifthenelse_sqle`
   THEN Try (MemBase)
   THEN D 0
   THEN OnMaybeHyp 6 (\h. (ParallelOp h THEN HypSubst' (-1) 0 THEN Complete (SqLeCD)))) }

---

Latex:

---

Latex:
\mforall{}[a,x1,y1,x2,y2:Base].
    if  a  then  x1  else  y1  fi    \msim{}  if  a  then  x2  else  y2  fi   
    supposing  ((\mexists{}z:Base.  (a  \msim{}  inl  z))  {}\mRightarrow{}  (x1  \msim{}  x2))  \mwedge{}  ((\mexists{}z:Base.  (a  \msim{}  inr  z  ))  {}\mRightarrow{}  (y1  \msim{}  y2))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  -1
  THEN  SqequalSqle
  THEN  BLemma  `ifthenelse\_sqle`
  THEN  Try  (MemBase)
  THEN  D  0
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  (ParallelOp  h  THEN  HypSubst'  (-1)  0  THEN  Complete  (SqLeCD))))

---

Home Index