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