proposition: Lemma matches_r_correct : \matches_correct /\ \nmatches_correct.
proof: Proof. apply matches_some_ind. intros y u θ θ'; simpl; unfold exmatch; case_eq (VM.find y θ). intros v Hv; case_eq (u =T v); intros Htv I; inversion_clear I in Hv. unfold subst_of_matching; rewrite Hv; simpl. by sym; apply (proj1 (beq_term_ok _ _)). intros _ I; inversion I as [Hadd]; clear I. by unfold subst_of_matching; rewrite VMF.add_eq_o. intros f g ts us _ θ _ Hveq Hfg. apply (proj1 (beq_term_ok _ _)); rewrite sub_fun, beq_fun. by rewrite Hveq, andb_true_r; apply (proj2 beq_symb_ok). intros θ; simpl; refl. intros t nt ts u nu us θ θ' Ω HΩθ IHΩθ HθΩ IHθΩ; simpl. rewrite <- IHΩθ, (beq_refl (@beq_term_ok Sig)), andb_true_l. eapply nmatches_submon with Ω t u; try hyp; intros x Hx. by unfold is_true; rewrite (nmatches_var_minP HθΩ), Hx, orb_true_r. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)