##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
nchange with ((S (len_list T l1)) = (S (len_list T l)));
##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
nchange with ((S (len_list T l1)) = (S (len_list T l)));