proposition: Lemma matches_var_minadded : forall u t m m', matches_r u t m = Some m' -> forall x, VM.mem x m = false -> VM.mem x m' -> VS.mem x (vars u).
proof: Proof. intros u t m m' H x Hmem₁ Hmem₂. by rewrite (matches_var_minP H) in Hmem₂; rewrite Hmem₁ in Hmem₂. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)