Li-Fan Chen says to YSITD
forall x. x=x
at Fri, Sep 14, 2018 9:33 PM