Сохранение информации при использовании индукции?

Я использую Coq Proof Assistant для реализации модели (небольшого) языка программирования (расширение реализации полулегкого Java Бруно Де Фрейна, Эрика Эрнста, Марио Зюдхолта). Одна вещь, которая постоянно возникает при использовании тактики индукции , - это как сохранить информацию, заключенную в конструкторы типов.

У меня есть подтип Prop, реализованный как

Inductive sub_type : typ -> typ -> Prop :=
| st_refl : forall t, sub_type t t
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub_type t2 t3 -> sub_type t1 t3
| st_extends : forall C D,
    extends C D ->
    sub_type (c_typ C) (c_typ D).

Hint Constructors sub_type.

, где extends - это механизм расширения класса, как показано в Java, а typ представляет два различных типа доступных типов,

Inductive typ : Set :=
| c_typ : cname -> typ
| r_typ : rname -> typ.

Примером того, где я хотел бы сохранить информацию о типе, является использование тактики индукции на гипотезе вроде

H: sub_type (c_typ u) (c_typ v)

Например, в

u : cname
v : cname
fsv : flds
H : sub_type (c_typ u) (c_typ v)
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

с использованием индукции H. отбрасывает всю информацию о u и v . Случай st_refl становится

u : cname
v : cname
fsv : flds
t : typ
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

. Как вы можете видеть, информация о том, что u и v связаны с конструкторами typ в ] H и, следовательно, до t , теряется. Что еще хуже, из-за этого Coq не может видеть, что u и v должны фактически быть одинаковыми в этом случае.

При использовании инверсии тактика на H Coq позволяет увидеть, что u и v одинаковы. Однако эта тактика здесь неприменима, поскольку мне нужны индукционные гипотезы, которые генерирует индукция , чтобы доказать случаи st_trans и st_extends .

Есть ли тактика. который сочетает в себе лучшее из инверсии и индукции , чтобы генерировать гипотезы индукции и выводить равенства без разрушения информации о том, что заключено в конструкторы? В качестве альтернативы, есть ли способ вручную получить нужную мне информацию? инверсия информации H и индукция информации H показывают, что множество преобразований применяется автоматически (особенно с инверсией ). Это побудило меня поэкспериментировать с тактикой изменения вместе с let ... в конструкции, но без какого-либо прогресса.