proposition: Lemma fsub_cons_rec x0 t n (ts : terms n) x k : x = x0+2+k -> fsub x0 (Vcons t ts) x = fsub (x0+1) ts x.
proof: Proof. intro. subst x. unfold fsub. destruct (le_lt_dec (x0+2+k) x0). lia. destruct (le_lt_dec (x0+2+k) (x0+1)). lia. destruct (le_lt_dec (x0+2+k) (x0+S n)); destruct (le_lt_dec (x0+2+k) (x0+1+n)); try lia. rewrite Vnth_cons. destruct (lt_ge_dec 0 (x0+2+k-x0-1)). apply Vnth_eq. clear. lia. lia. refl. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)