nlemma symmetric_eqasttype_aux1
: ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false.
#x1; #x2; #y2; ncases y2; nnormalize;
nlemma symmetric_eqasttype_aux1
: ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false.
#x1; #x2; #y2; ncases y2; nnormalize;