Step * of Lemma inr-one-one'

No Annotations
[A,B:Type]. ∀[x,y:B].  y ∈ supposing (inr (inr ) ∈ (A B)
BY
Auto }


Latex:


Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[x,y:B].    x  =  y  supposing  (inr  x  )  =  (inr  y  )


By


Latex:
Auto




Home Index