proposition: Lemma decomposition_e_unfold_normal : forall pb Inv_pb, decomposition_step_e (OK (Normal _ pb) Inv_pb) = OK (decomposition_step pb) (inv_solved_part_e _ (or_introl _ Inv_pb)).
proof: Proof. intros pb Inv_pb; simpl; trivial. Defined.
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)