nlemma eqastbasetype_to_eq : ∀b1,b2.eq_astbasetype b1 b2 = true → b1 = b2.
#b1; #b2; ncases b1; ncases b2; nnormalize;
##[ ##1,5,9: #H; napply refl_eq
nlemma eqastbasetype_to_eq : ∀b1,b2.eq_astbasetype b1 b2 = true → b1 = b2.
#b1; #b2; ncases b1; ncases b2; nnormalize;
##[ ##1,5,9: #H; napply refl_eq