Tree @master (Download .tar.gz)
incorrect-reflexivity.eqthy.md @master — view markup · raw · history · blame
axiom (idright) mul(A, e) = A
axiom (idleft) mul(e, A) = A
axiom (assoc) mul(A, mul(B, C)) = mul(mul(A, B), C)
theorem
A = mul(A, e)
proof
A = A
A = mul(A, e) [by reflexivity]
qed