Step
*
of Lemma
typed-null-ite
∀[x,y:Top List]. ∀[b:𝔹].  null(if b then x else y fi ) = if b then null(x) else null(y) fi 
BY
{ xxx(Auto THEN SplitOnConclITE THEN Auto)xxx }
Latex:
Latex:
\mforall{}[x,y:Top  List].  \mforall{}[b:\mBbbB{}].    null(if  b  then  x  else  y  fi  )  =  if  b  then  null(x)  else  null(y)  fi 
By
Latex:
xxx(Auto  THEN  SplitOnConclITE  THEN  Auto)xxx
Home
Index