refl>

Theorem.

Arguments:

x (obj), y (obj),

Assertions:

((xeqy)to(yeqy))

Proof:

Hyp Ref Line Expr
refl<1((yeqx)to(yeqy))
1ax-sym2((xeqy)to(yeqy))