let A, B be MP-wff; :: thesis: ( (#) A = (#) B implies A = B )
set AA = (elementary_tree 1) --> [1,1];
assume A1: (#) A = (#) B ; :: thesis: A = B
<*0*> in dom ((elementary_tree 1) --> [1,1]) by Lm3;
hence A = B by A1, Th7; :: thesis: verum