Step
*
of Lemma
inr-one-one
∀[A,B:Type]. ∀[x,y:B].  uiff((inr x ) = (inr y ) ∈ (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