proposition: Lemma matches_var_min_comb : \matches_var_min /\ \nmatches_var_min.
proof: Proof. apply matches_some_ind. simpl; intros y t θ θ' H x. by rewrite VSF.singleton_b, vmap_eqb; eapply exmatches_var_min; eauto. by intros f _ ts _ θ θ' _ H _ x; rewrite AVariables.vars_fun. by intros θ x; simpl; rewrite VSF.empty_b, orb_false_r. intros u nu us _ _ _ θ θ' Ω _ HΩθ' _ HθΩ x. simpl; rewrite VSF.union_b, (HΩθ' x), (HθΩ x). by case (VM.mem x θ); simpl; try rewrite orb_comm. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)