proposition: Lemma sub_shift_incl s r : vars r [= vars l -> sub s r = sub (sub_comp s shift_inv_sub) (shift r).
proof: Proof. intro. unfold shift. rewrite sub_sub. apply sub_eq. intros. rewrite sub_comp_assoc. unfold sub_comp. simpl. f_equal. unfold shift_inv_var. rewrite plus_minus_eq. assert (Inb eq_nat_dec x (vars l) = true). apply Inb_intro. apply H. hyp. rewrite H1. case (le_lt_dec p (x+p)); intro. refl. lia. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)