proposition: Lemma lforall_is_sol_solved_eqn : forall s x u, s x = sub s u -> forall l, lforall (is_sol_solved_eqn s) (map (solved_eqn_sub (single x u)) l) <-> lforall (is_sol_solved_eqn s) l.
proof: Proof. induction l; simpl. tauto. destruct a. split_all; try tauto. revert H0. unfold is_sol_solved_eqn, solved_eqn_sub. simpl. rewrite sub_sub. intro. rewrite H0. apply sub_comp_single. hyp. revert H0. unfold is_sol_solved_eqn, solved_eqn_sub. simpl. rewrite sub_sub. intro. rewrite H0. sym. apply sub_comp_single. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)