proposition: Lemma lforall_is_sol_eqn_combine : forall s n (v v0 : terms n), lforall (is_sol_eqn s) (combine (list_of_vec v) (list_of_vec v0)) <-> Vmap (sub s) v = Vmap (sub s) v0.
proof: Proof. induction v; simpl; intros. VOtac. simpl. tauto. VSntac v0. simpl. unfold is_sol_eqn at 1. simpl. rewrite IHv. split_all. rewrite H1, H0. refl. Veqtac. hyp. Veqtac. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)