proposition: Lemma is_sol_sub : forall s s' p, is_sol s p -> is_sol (sub_comp s' s) p.
proof: Proof. intros s s' p. destruct p. 2: auto. destruct p. destruct l0. simpl. split_all. apply is_sol_solved_eqns_sub. hyp. destruct e. simpl. split_all. apply is_sol_solved_eqns_sub. hyp. apply is_sol_eqn_sub. hyp. revert H1. elim l0; clear l0; simpl; split_all. apply is_sol_eqn_sub. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)