Step * of Lemma apply-ifthenelse-pi1

[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 )
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  )  \msim{}  if  b  then  fst(x)  else  fst(y)  fi  )


By


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




Home Index