fact: Definition matching : list (term * term) -> option substitution := Fix wf_size (fun l => option substitution) F_matching.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)