Step * of Lemma apply-ifthenelse-pi1-eq

[T1,U1,T2,U2:Type]. ∀[x:T1 × U1]. ∀[y:T2 × U2]. ∀[b:𝔹].
  ((fst(if then else fi )) if then fst(x) else fst(y) fi  ∈ if then T1 else T2 fi )
BY
((UnivCD THENA Auto) THEN (-1) THEN Reduce 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