proposition: Lemma Lt_step : forall p, solved p = false -> Lt' (step p) p.
proof: Proof. destruct p. destruct p. destruct e. simpl. discr. intro. destruct e as [t0 t1]. destruct t0 as [?|? t0]; destruct t1 as [?|? t1]. simpl. mem. case_beq_nat n n0; unfold Lt'. apply Lt_cons. apply Lt_eqns_subs_r. simpl. mem. hyp. unfold step. rewrite vars_fun. simpl. case_eq (mem n (vars_vec t1)); intro H0; unfold Lt'. trivial. apply Lt_eqns_subs_l. hyp. unfold step. rewrite vars_fun. simpl. case_eq (mem n (vars_vec t0)); intro H0; unfold Lt'. trivial. apply Lt_eqns_subs_r. hyp. simpl. case_eq (beq_symb f f0); intro H0; unfold Lt'. apply Lt_combine. hyp. trivial. simpl. discr. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)