fact: Parameter matching_is_complete : forall t1 t2 Wt1 Wt2 sigma, well_formed_cf_subst sigma -> apply_cf_subst sigma t1 = t2 -> (exists sigma', In sigma' (matching t1 t2 Wt1 Wt2) /\ (forall v, occurs_in_term v t1 -> apply_cf_subst sigma (Var v) = apply_cf_subst sigma' (Var v))).
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)