proposition: Lemma fsub_nth x0 n (ts : terms n) x (h1 : x0 < x) (h2 : x <= x0+n) : fsub x0 ts x = Vnth ts (lt_pm h1 h2).
proof: Proof. unfold fsub. case (le_lt_dec x x0); intro. lia. case (le_lt_dec x (x0+n)); intro. apply Vnth_eq. refl. lia. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)