proposition: Lemma inject_terms_nth : forall i n (ts : terms n) (H : Vforall max_le ts) (ip : i < n), Vnth (inject_terms H) ip = inject_term (Vforall_nth ip H).
proof: Proof. induction i; intros. destruct ts. lia. simpl. match goal with |- inject_term ?Hl = inject_term ?Hr => rewrite (le_unique Hl Hr) end. refl. destruct ts. lia. simpl. rewrite IHi. match goal with |- inject_term ?Hl = inject_term ?Hr => rewrite (le_unique Hl Hr) end. refl. Qed.
imports: CoLoR(ATerm VecUtil AInterpretation LogicUtil NatUtil)