refl<

Theorem.

Arguments:

x (obj), y (obj),

Assertions:

((xeqy)to(xeqx))

Proof:

Hyp Ref Line Expr
ax-tr1((xeqy)to((yeqx)to(xeqx)))
ax-sym2((xeqy)to(yeqx))
1, 2mpd3((xeqy)to(xeqx))