---

Step * of Lemma apply-ifthenelse-pi1-eq

∀[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  ((fst(if b then x else y fi )) = if b then fst(x) else fst(y) fi  ∈ if b then T1 else T2 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{}].
    ((fst(if  b  then  x  else  y  fi  ))  =  if  b  then  fst(x)  else  fst(y)  fi  )


By

---

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

---

Home Index