proposition: Lemma map_path b x' p' (Bb : rel_base b) : ~~ has (preim h b) (belast x' p') -> path e (h x') (map h p') = path e' x' p'.
proof: Proof. by elim: p' x' => [|y' p' IHp'] x' //= /norP[/Bb-> /IHp'->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)