proposition: Lemma matching_unfold : forall l : list (term*term), matching l = @F_matching l (fun y _ => matching y).
proof: Proof. intros lpb; unfold matching. refine (Fix_eq _ _ _ _ lpb). clear lpb; intros lpb F G H. unfold F_matching; destruct lpb as [ | [patt subj] lpb]; simpl; auto. destruct patt as [x | f l]; destruct subj as [y | g m]; simpl; auto. rewrite H; trivial. rewrite H; trivial. case (eq_symb_bool f g); trivial. destruct l as [ | pat lpat]; destruct m as [ | sub lsub]; trivial. rewrite H; trivial. do 2 rewrite H; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)