proposition: Lemma matches_correct : forall u t θ, matches u t = Some θ -> u ! θ = t.
proof: Proof. intros u t θ; unfold matches. case_eq (matches_r u t VM.empty); try discr; intros Ω HΩ. inversion_clear 1; apply (proj1 matches_r_correct) with VM.empty. hyp. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)