let p, q be MP-variable; :: thesis: ( @ p = @ q implies p = q )
A1: {} in elementary_tree 0 by TREES_1:47;
assume A2: @ p = @ q ; :: thesis: p = q
p = (@ p) . {} by A1, FUNCOP_1:13
.= q by A1, A2, FUNCOP_1:13 ;
hence p = q ; :: thesis: verum