proposition: Lemma sub_fsub_inf n (ts : terms n) m : forall t, maxvar t <= m -> sub (fsub m ts) t = t.
proof: Proof. set (P := fun t => maxvar t <= m -> sub (fsub m ts) t = t). change (forall t, P t). apply term_ind_forall. unfold P, fsub. simpl. intros. case (le_lt_dec v m); intro. refl. case (le_lt_dec v (m+n)); intro. lia. refl. intros. unfold P. intro. simpl sub. f_equal. apply Vmap_eq_id. eapply Vforall_impl. apply H. intros. apply H2. eapply maxvar_le_arg with (f := f). apply H0. hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)