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