proposition: Lemma matching_correct : forall pb sigma, matching pb = Some sigma -> ((forall v p s, In v (var_list p) -> In (p,s) pb -> find eq_var_bool v sigma <> None) /\ (forall v, find eq_var_bool v sigma <> None -> exists p, exists s, In (p,s) pb /\ In v (var_list p)) /\ (forall p s, In (p,s) pb -> apply_subst sigma p = s)).
proof: Proof. intros pb sigma H; generalize (matching_correct_aux pb H); intuition. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)