proposition: Lemma step_correct : forall s p, is_sol s p <-> is_sol s (step p).
proof: Proof. intros s p. destruct p. 2: simpl; tauto. destruct p. destruct l0. simpl. split_all. destruct e as [[?|? t0] [?|? t1]]. simpl. unfold is_sol_eqn. mem. simpl. case_beq_nat n n0; simpl. tauto. unfold is_sol_solved_eqn. simpl. split_all. rewrite is_sol_solved_eqns_map; auto. rewrite is_sol_eqns_map; auto. rewrite is_sol_solved_eqns_map in H2; auto. rewrite is_sol_eqns_map in H1; auto. Opaque vars. simpl. set (u := Fun f t1). unfold is_sol_eqn. simpl fst. simpl snd. simpl sub at 1. case_eq (mem n (vars u)). split_all; try contr. ded (wf_term_var H1 H). discr. unfold is_sol, is_sol_solved_eqns. simpl lforall. unfold is_sol_solved_eqn at 2. simpl fst. simpl snd. split_all. rewrite lforall_is_sol_solved_eqn; auto. rewrite is_sol_eqns_map; auto. rewrite lforall_is_sol_solved_eqn in H2; hyp. rewrite is_sol_eqns_map in H1; hyp. simpl. set (u := Fun f t0). unfold is_sol_eqn. simpl fst. simpl snd. simpl sub at 2. case_eq (mem n (vars u)). split_all; try contr. symmetry in H1. ded (wf_term_var H1 H). discr. unfold is_sol, is_sol_solved_eqns. simpl lforall. unfold is_sol_solved_eqn at 2. simpl fst. simpl snd. split_all. rewrite lforall_is_sol_solved_eqn; auto. rewrite is_sol_eqns_map; auto. rewrite lforall_is_sol_solved_eqn in H2; hyp. rewrite is_sol_eqns_map in H1; hyp. simpl. unfold is_sol_eqn. unfold fst, snd. rewrite !sub_fun. case_beq_symb f f0. simpl. unfold is_sol_eqns at 2. rewrite lforall_app, lforall_is_sol_eqn_combine. split_all. Funeqtac. hyp. apply args_eq. hyp. split_all; try contr. Funeqtac. rewrite (beq_refl (@beq_symb_ok Sig)) in H. discr. Transparent vars. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)