---

Step * of Lemma apply-ifthenelse-pi2-eq

∀[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  ((snd(if b then x else y fi )) = if b then snd(x) else snd(y) fi  ∈ if b then U1 else U2 fi )
BY
{ ((UnivCD THENA Auto) THEN D (-1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T1,U1,T2,U2:Type].  \mforall{}[x:T1  \mtimes{}  U1].  \mforall{}[y:T2  \mtimes{}  U2].  \mforall{}[b:\mBbbB{}].
    ((snd(if  b  then  x  else  y  fi  ))  =  if  b  then  snd(x)  else  snd(y)  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  (-1)  THEN  Reduce  0  THEN  Auto)

---

Home Index