#f1 elim (gr_map_split_tl f1) #H1 #f2 #H
[ lapply (gr_sle_push_sn_tl … H … H1) -H //
| elim (gr_sle_inv_next_sn … H … H1) -H //
#f1 elim (gr_map_split_tl f1) #H1 #f2 #H
[ lapply (gr_sle_push_sn_tl … H … H1) -H //
| elim (gr_sle_inv_next_sn … H … H1) -H //