proposition: Lemma solved_inv : forall p, solved (step p) = false -> solved p = false.
proof: Proof. destruct p. 2: discr. destruct p. destruct e. discr. destruct e. refl. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)