proposition: Lemma step_wf : forall p, problem_wf p -> problem_wf (step p).
proof: Proof. intro. destruct p. 2: auto. destruct p. destruct e. auto. destruct e as [[?|? t0] [?|? t1]]. simpl. mem. case_beq_nat n n0; simpl. intuition. revert H1. elim s; simpl; intuition. mem. rewrite H. split_all. eapply lforall_notin_solved_eqn_1. simpl. mem. hyp. apply H1. eapply solved_eqns_wf_map'. simpl. mem. hyp. hyp. apply H1. revert H1. elim s; simpl; split_all. unfold notin_vars_solved_eqn. simpl. unfold notin_eqn in H2. simpl in H2. split_all. apply notin_map. simpl. mem. hyp. apply lforall_notin_r. hyp. Opaque vars. simpl. set (u := Fun f t1). split_all. case_eq (mem n (vars u)); simpl; split_all. eapply lforall_notin_solved_eqn_1'. hyp. apply H0. eapply solved_eqns_wf_map. hyp. hyp. apply H0. apply lforall_notin_vars_solved_eqn_2 with e0. hyp. apply notin_map. hyp. apply lforall_notin_l. hyp. simpl. set (u := Fun f t0). split_all. case_eq (mem n (vars u)); simpl; split_all. eapply lforall_notin_solved_eqn_1. hyp. apply H0. eapply solved_eqns_wf_map'. hyp. hyp. apply H0. apply lforall_notin_vars_solved_eqn_2' with e0. hyp. apply notin_map. hyp. apply lforall_notin_r. hyp. simpl. case_beq_symb f f0; simpl; split_all. revert H0. elim s; simpl; split_all. revert H1. unfold notin_eqn. simpl. rewrite !vars_fun. revert H3. unfold notin. simpl. rewrite lforall_app. split_all. apply lforall_notin_eqn_combine; hyp. Transparent vars. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)