proposition: Lemma disjoint_vars_com t u : disjoint_vars t u -> disjoint_vars u t.
proof: Proof. unfold disjoint_vars. intros. apply sym_eq. apply (H x); hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)