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