proposition: Lemma decompose_unfold : forall u : exc_pb_ok, decompose u = @F_decompose u (fun u' _ => decompose u').
proof: Proof. intros u; unfold decompose; apply Fix_eq with (P:= (fun _: exc_pb_ok => exc unification_problem)); clear u. intros [ [pb | pb | ] Inv_pb] f g H; simpl; [ rewrite H | idtac | idtac ]; trivial. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)