proposition: Lemma pw_disjoint_vars_cons : forall t l, pw_disjoint_vars l -> (forall u, In u l -> disjoint_vars t u) -> pw_disjoint_vars (t :: l).
proof: Proof. intros. unfold pw_disjoint_vars. simpl. intros. destruct H1; destruct H2. subst t0. subst u. apply disjoint_vars_refl. subst t0. auto. subst u. apply disjoint_vars_com. apply H0. exact H1. apply H; hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil VecMax NatUtil ASubstitution)