proposition: Lemma fpath_finv x p : fpath finv x p = fpath f (last x p) (rev (belast x p)).
proof: Proof. exact: (@fpath_finv_in T _ (in2W _)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)