proposition: Lemma matches_complete_ext : forall u t θ, u!θ = t -> exists Ω, ( matches u t = Some Ω /\ forall x, VS.mem x (vars u) -> θ x = Ω x).
proof: Proof. intros u t θ H; case_eq (matches u t). intros Ω HΩ; exists Ω; split; [refl | idtac]. intros x Hxu; apply subeq_inversion with u. by rewrite H; sym; apply matches_correct. by apply (proj2 (AVariables.in_vars_mem _ _)). intros Habs; elim (matches_complete H Habs). Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)