proposition: Lemma exmatch_mon : forall θ θ' x t, exmatch θ x t = Some θ' -> forall y, VM.mem y θ -> VM.find y θ = VM.find y θ'.
proof: Proof. intros θ θ' x t; unfold exmatch; case_eq (VM.find x θ). by intros u H; case (t =T u); intros I; inversion_clear I. intros H I; inversion_clear I; intros y Hyθ. sym; apply VMF.add_neq_o; intros Hxy; subst y. rewrite VMF.mem_find_b in Hyθ; rewrite H in Hyθ. discr. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)