Тактическое абстрагирование над субтермом типа цели

В качестве грубой и необученной основы, в HoTT , один выводит чертовски из индуктивно определенного типа

Inductive paths {X : Type } : X -> X -> Type :=
 | idpath : forall x: X, paths x x.

, который допускает очень общую конструкцию

Lemma transport {X : Type } (P : X -> Type ){ x y : X} (γ : paths x y):
  P x -> P y.
Proof.
 induction γ.
 exact (fun a => a).
Defined.

Лемма транспорт будет в основе тактики HoTT «заменить» или «переписать»; Уловка, насколько я понимаю, будет заключаться в том, чтобы предположить цель, которую вы или я можем абстрактно распознать как

...
H : paths x y
[ Q : (G x) ]
_____________
(G y)

, чтобы выяснить, что является необходимым зависимым типом G, чтобы мы могли применить (транспорт GH) . Пока все, что я понял, это то, что

Ltac transport_along γ :=
match (type of γ) with 
| ?a ~~> ?b =>
 match goal with
 |- ?F b => apply (transport F γ)
 | _ => idtac "apparently couldn't abstract" b "from the goal."  end 
| _ => idtac "Are you sure" γ "is a path?" end.

недостаточно общий. То есть первый idtac используется довольно часто.

Вопрос

[Есть ли | что такое] Правильная вещь ?