proposition: Lemma matches_submon : forall u t θ, u ! \S(θ) = t -> (forall x, VS.mem x (vars u) -> VM.mem x θ) -> forall u' t' θ', matches_r u' t' θ = Some θ' -> u ! \S(θ') = t.
proof: Proof. intros u t θ Hsub Hdom u' t' θ' Hθθ'; subst t. apply sub_eq; intros x Hx; unfold subst_of_matching. rewrite (matches_monP Hθθ'); try refl. by apply Hdom; unfold is_true; apply (proj1 (AVariables.in_vars_mem _ _)). Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)