proposition: Lemma wf_mk_problem : forall u v, problem_wf (mk_problem u v).
proof: Proof. unfold mk_problem. simpl. auto. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)