fact: Parameter matching_complete : forall pb sigma, (forall p s, In (p,s) pb -> apply_subst sigma p = s) -> match matching pb with | Some tau => forall v p s, In v (var_list p) -> In (p,s) pb -> apply_subst tau (Var v) = apply_subst sigma (Var v) | None => False end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)