Step * of Lemma inr_equal

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


Latex:


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


By


Latex:
Auto




Home Index