From Undecidability.TM.Code.List Require Export Nth Cons_constant App Length Rev Concat_Repeat.
From Undecidability Require Import HoareLogic.
Ltac hstep_ListTM :=
match goal with
| [ |- TripleT ?P ?k (Nth' _ _) ?Q ] => eapply Nth'_SpecT_size
end.
Smpl Add hstep_ListTM : hstep_Spec.
From Undecidability Require Import HoareLogic.
Ltac hstep_ListTM :=
match goal with
| [ |- TripleT ?P ?k (Nth' _ _) ?Q ] => eapply Nth'_SpecT_size
end.
Smpl Add hstep_ListTM : hstep_Spec.