added index injectivity axioms for datatypes; insertionsort.fst now verifies