proposition: Lemma matches_mon_comb : \matches_mon /\ \nmatches_mon.
proof: Proof. apply matches_some_ind; auto. by intros x t θ θ'; apply exmatch_mon. intros _ _ _ _ _ _ θ θ' Ω _ HΩθ' _ HθΩ x Hx. trans (VM.find x Ω); [by apply HθΩ | idtac]. apply HΩθ'; unfold is_true; rewrite <- Hx; rewrite !VMF.mem_find_b. by rewrite (HθΩ x Hx). Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)