proposition: Lemma fsub_cons x0 t n (ts : terms n) x : x = x0+1 -> fsub x0 (Vcons t ts) x = t.
proof: Proof. intro. subst x. unfold fsub. case (le_lt_dec (x0+1) x0); intro. lia. case (le_lt_dec (x0+1) (x0+S n)); intro. rewrite Vnth_cons_head. refl. lia. lia. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)