for A being MP-wff holds ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff