proposition: Lemma matches_complete : forall u t θ, u!θ = t -> matches u t <> None.
proof: Proof. intros u t θ H; unfold matches. case_eq (matches_r u t VM.empty). by intros; discr. intros Habd _; eapply (proj1 matches_r_complete); [idtac|ehyp]. exists θ; rewrite <- H; apply sub_eq; intros x _. by unfold compose; rewrite VMF.empty_o. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)