nrewrite > (symmetric_eqstr (str_elem si1) (str_elem si2));
nrewrite > (symmetric_eqnat (id_elem si1) (id_elem si2));
napply refl_eq.
nrewrite > (symmetric_eqstr (str_elem si1) (str_elem si2));
nrewrite > (symmetric_eqnat (id_elem si1) (id_elem si2));
napply refl_eq.