Step * of Lemma inr_eq_inl

[A,B:Type]. ∀[x:A]. ∀[y:B].  uiff((inr (inl x) ∈ (A B);False)
BY
Auto }


Latex:


Latex:
\mforall{}[A,B:Type].  \mforall{}[x:A].  \mforall{}[y:B].    uiff((inr  y  )  =  (inl  x);False)


By


Latex:
Auto




Home Index