proposition: Lemma well_formed_init_pb : forall t1 t2, well_formed_cf t1 -> well_formed_cf t2 -> well_formed_pb (init_pb t1 t2).
proof: Proof. intros t1 t2 Wt1 Wt2; unfold well_formed_pb, init_pb; simpl; intuition. injection H0; intros; subst t0; trivial. injection H0; intros; subst t3; trivial. absurd (None = Some p); trivial; discriminate. Qed.
imports: Coq(Arith List Wellfounded Wf_nat) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory ac matching dickson matching_well_formed matching_well_founded matching_sound matching_complete dickson)