proposition: Lemma lforall_notin_eqn_combine : forall x n (v1 v2 : terms n), mem x (vars_vec v1) = false -> mem x (vars_vec v2) = false -> lforall (notin_eqn x) (combine (list_of_vec v1) (list_of_vec v2)).
proof: Proof. induction v1; simpl; intros. trivial. VSntac v2. simpl. autorewrite with mem in H. destruct (orb_false_elim H). assert (mem x (vars (Vhead v2)) = false /\ mem x (vars_vec (Vtail v2)) = false). rewrite H1 in H0. simpl in H0. autorewrite with mem in H0. destruct (orb_false_elim H0). split_all. split_all. unfold notin_eqn. simpl. split_all. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)